How to substitute into an expression

Stream: new members

[Dominic Steinitz]

I have

import Mathlib

open Manifold

open SmoothManifoldWithCorners

open MulAction

open Bundle

example {G B : Type*} {E : B → Type*} (k n : ℕ)
[TopologicalSpace B]
[ChartedSpace (EuclideanSpace ℝ (Fin n)) B]
[TopologicalSpace G]
[ChartedSpace (EuclideanSpace ℝ (Fin k)) G]
[Group G]
[MulAction G P]
[TopologicalGroup G]
[TopologicalSpace (TotalSpace G E)]
[(b : B) → TopologicalSpace (E b)]
[LieGroup (𝓡 k) G]
[FiberBundle G E] (g g': G) (p q : P)
(h_free : stabilizer G p = ⊥) :
  true := by
    have h3 : orbitRel G P q p ↔ q ∈ orbit G p := by apply orbitRel_apply
    have h4 : q ∈ orbit G p ↔ ∃ g : G, g • p = q := by apply mem_orbit_iff
    have h5 : orbitRel G P q p ↔ ∃ g : G, g • p = q := by
      rw [h3, h4]

    have h6 : orbitRel G P p p ↔ ∃ g : G, g • p = p := by
      apply h5

    trivial

but I get

tactic 'apply' failed, failed to unify
  (orbitRel G P) q p ↔ ∃ g, g • p = q
with
  (orbitRel G P) p p ↔ ∃ g, g • p = p

How do I tell lean to replace q with p?

[Kevin Buzzard]

You can't replace 2 with 3 in the theorem 2+2=4 so I'm not sure I really understand the question

[Kevin Buzzard]

Do you want a version of h5 saying "for all q, ..."?

[Dominic Steinitz]

Something like this so yes quantified by $\forall$ - thanks very much

import Mathlib

open Manifold

open SmoothManifoldWithCorners

open MulAction

open Bundle

lemma foo {G P : Type*} (p q : P)
[Group G]
[MulAction G P] : (orbitRel G P) q p ↔ ∃ (g : G), g • p = q := by
  have h3 : orbitRel G P q p ↔ q ∈ orbit G p := by apply orbitRel_apply
  have h4 : q ∈ orbit G p ↔ ∃ g : G, g • p = q := by apply mem_orbit_iff
  have h5 : orbitRel G P q p ↔ ∃ g : G, g • p = q := by
    rw [h3, h4]
  exact h5

example {G B : Type*} {E : B → Type*} (k n : ℕ)
[TopologicalSpace B]
[ChartedSpace (EuclideanSpace ℝ (Fin n)) B]
[TopologicalSpace G]
[ChartedSpace (EuclideanSpace ℝ (Fin k)) G]
[Group G]
[MulAction G P]
[TopologicalGroup G]
[TopologicalSpace (TotalSpace G E)]
[(b : B) → TopologicalSpace (E b)]
[LieGroup (𝓡 k) G]
[FiberBundle G E] (g g': G) (p q r : P) :
  true := by

    have h_refl : orbitRel G P p p := by
      have hr1 : orbitRel G P p p ↔ ∃ g : G, g • p = p := by
        apply foo p p
      have hr2 : ∃ g : G, g • p = p := Exists.intro 1 (one_smul _ _)
      apply hr1.mpr hr2

    have h_symm : orbitRel G P p q -> orbitRel G P q p := by
      intro h
      have hs1 : ∃ (g : G), g • q = p := by
        apply (foo q p).mp h
      have hs2 : ∃ (g : G), g • p = q :=
        Exists.elim hs1 (λ g => λ hg =>
         by
          have hs2a : g • q = p := hg
          have hs2b :  q = g⁻¹ • p := by
            calc q = (1 : G) • q := by apply (Eq.symm (one_smul _ _))
            _ = (g⁻¹ * g) • q := by rw [inv_mul_cancel]
            _ = g⁻¹ • (g • q) := by apply (mul_smul g⁻¹ g q)
            _ = g⁻¹ • p := by rw [hs2a]
          exact Exists.intro g⁻¹ (Eq.symm hs2b))
      have hs3 : orbitRel G P q p := by
        apply (foo p q).mpr hs2
      exact hs3

    have h_tran : orbitRel G P p q -> orbitRel G P q r -> orbitRel G P p r := by
      intro h
      sorry

    trivial

[Dominic Steinitz]

And I now see that this has been done for me: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/GroupTheory/GroupAction/Defs.lean#L303