mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
H : Type u_7
E : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
⊢ IsSubmersion I I n id

Tactic:
use PUnit, by infer_instance, by infer_instance

Goal state after:
case h
𝕜 : Type u_1
H : Type u_7
E : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
⊢ IsSubmersionOfComplement PUnit.{u + 1} I I n id
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric

Goal state before:
pp: E : Type u_1
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
H : Type u_2
inst✝¹² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁷ : TopologicalSpace (TotalSpace F V)
inst✝⁶ : (x : M) → NormedAddCommGroup (V x)
inst✝⁵ : (x : M) → InnerProductSpace ℝ (V x)
inst✝⁴ : FiberBundle F V
σ τ : (x : M) → V x
cov : CovariantDerivative I F V
inst✝³ : VectorBundle ℝ F V
inst✝² : IsContMDiffRiemannianBundle I 1 F V
X : (x : M) → TangentSpace I x
inst✝¹ : ContMDiffVectorBundle 1 F V I
inst✝ : FiniteDimensional ℝ F
x : M
hσ : MDiffAt (T% σ) x
hτ : MDiffAt (T% τ) x
⊢ (derivMetricTensorAux I cov σ τ x) (X x) =
    ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) - (fun x ↦ inner ℝ ((fun x ↦ (↑cov σ x) (X x)) x) (τ x)) x -
      (fun x ↦ inner ℝ (σ x) ((fun x ↦ (↑cov τ x) (X x)) x)) x

Tactic:
derivMetricTensorAux_apply

Goal state after:
E : Type u_1
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
H : Type u_2
inst✝¹² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁷ : TopologicalSpace (TotalSpace F V)
inst✝⁶ : (x : M) → NormedAddCommGroup (V x)
inst✝⁵ : (x : M) → InnerProductSpace ℝ (V x)
inst✝⁴ : FiberBundle F V
σ τ : (x : M) → V x
cov : CovariantDerivative I F V
inst✝³ : VectorBundle ℝ F V
inst✝² : IsContMDiffRiemannianBundle I 1 F V
X : (x : M) → TangentSpace I x
inst✝¹ : ContMDiffVectorBundle 1 F V I
inst✝ : FiniteDimensional ℝ F
x : M
hσ : MDiffAt (T% σ) x
hτ : MDiffAt (T% τ) x
⊢ ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) - inner ℝ ((↑cov σ x) (X x)) (τ x) - inner ℝ (σ x) ((↑cov τ x) (X x)) =
    ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) - (fun x ↦ inner ℝ ((fun x ↦ (↑cov σ x) (X x)) x) (τ x)) x -
      (fun x ↦ inner ℝ (σ x) ((fun x ↦ (↑cov τ x) (X x)) x)) x
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: case intro.e_a.mk
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ 1 = Fintype.card ↑(carrier (Quot.mk (⇑(IsConj.setoid G)) g))

Tactic:
rw [eq_comm, ← Set.toFinset_card, Finset.card_eq_one]

Goal state after:
case intro.e_a.mk
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ ∃ a, (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).toFinset = {a}
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n k : ℕ
⊢ r 1 ^ k = r ↑k

Tactic:
simp only [r_pow, one_mul]

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
hn : Odd n
⊢ commProb (DihedralGroup n) = (↑n + 3) / (4 * ↑n)

Tactic:
rw [commProb_def', DihedralGroup.card_conjClasses_odd hn, nat_card]
  qify [show 2 ∣ n + 3 by rw [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, Nat.odd_iff.mp hn]]
  rw [div_div, ← mul_assoc]
  congr
  norm_num

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
h2 : Even n
⊢ n ≠ 1

Tactic:
rintro rfl

Goal state after:
h0 : 1 ≠ 0
h2 : Even 1
⊢ False
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
h1 : n ≠ 1
h2 : Odd n
⊢ n ≠ 0

Tactic:
rintro rfl

Goal state after:
h1 : 0 ≠ 1
h2 : Odd 0
⊢ False
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : Monoid P
P' : Type u_4
inst✝ : Monoid P'
f : P →* P'
g₁ : M →* P
g₂ : N →* P
⊢ (f.comp (lift g₁ g₂)).comp inr = (lift (f.comp g₁) (f.comp g₂)).comp inr

Tactic:
by
    rw [MonoidHom.comp_assoc, lift_comp_inr, lift_comp_inr]

Goal state after:
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ (MonoidHom.snd M N).comp (fst.prod snd) = snd

Tactic:
MonoidHom.snd_comp_prod

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ snd = snd
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
this : cs.simple = ⇑cs.mulEquiv.symm ∘ PresentedGroup.of
⊢ cs.mulEquiv.symm.toMonoidHom.range = ⊤

Tactic:
exact MonoidHom.range_eq_top.2 (MulEquiv.surjective _)

Goal state after:
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x y : B
hy :
  ‖Trivialization.symmL ℝ (trivializationAt F E x) x ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
    2
A :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x ∘SL
      Trivialization.symmL ℝ (trivializationAt F E x) x =
    ContinuousLinearMap.id ℝ F
this :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y =
    ContinuousLinearMap.id ℝ F ∘SL Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y
⊢ ‖(Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x ∘SL
          Trivialization.symmL ℝ (trivializationAt F E x) x) ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
    (1 + ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖) * 2

Tactic:
comp_assoc,

Goal state after:
B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x y : B
hy :
  ‖Trivialization.symmL ℝ (trivializationAt F E x) x ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
    2
A :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x ∘SL
      Trivialization.symmL ℝ (trivializationAt F E x) x =
    ContinuousLinearMap.id ℝ F
this :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y =
    ContinuousLinearMap.id ℝ F ∘SL Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y
⊢ ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x ∘SL
        Trivialization.symmL ℝ (trivializationAt F E x) x ∘SL
          Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
    (1 + ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖) * 2
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case neg
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx ≠ some i
he : rcons { head := m, tail := w, fstIdx_ne := h } = rcons { head := m', tail := w', fstIdx_ne := h' }
hm : ¬m = 1
hm' : ¬m' = 1
⊢ { head := m, tail := w, fstIdx_ne := h } = { head := m', tail := w', fstIdx_ne := h' }

Tactic:
have : m = m' ∧ w.toList = w'.toList := by
      simpa [cons, rcons, dif_neg hm, dif_neg hm', eq_self_iff_true, Subtype.mk_eq_mk,
        heq_iff_eq, ← Subtype.ext_iff] using he

Goal state after:
case neg
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx ≠ some i
he : rcons { head := m, tail := w, fstIdx_ne := h } = rcons { head := m', tail := w', fstIdx_ne := h' }
hm : ¬m = 1
hm' : ¬m' = 1
this : m = m' ∧ w.toList = w'.toList
⊢ { head := m, tail := w, fstIdx_ne := h } = { head := m', tail := w', fstIdx_ne := h' }
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
m' : ℤ
⊢ (if Even m' then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m' / ↑2) =
    (if Even (↑(M.M i i' * 2) - m') then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((↑(M.M i i' * 2) - m') / ↑2)

Tactic:
push_cast

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
m' : ℤ
⊢ (if Even m' then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m' / 2) =
    (if Even (↑(M.M i i') * 2 - m') then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - m') / 2)
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ w = 1 → cs.length w = 0

Tactic:
rintro rfl

Goal state after:
case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ cs.length 1 = 0
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos.mp
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList = []
m₂ m₁ : M (w.toList.head hnil).fst
hw : ⟨(w.toList.head hnil).fst, m₁⟩ ∉ w.toList.tail
hm1 : ¬m₁ = 1
⊢ m₁ = m₂ * (w.toList.head ⋯).snd →
    (∃ m', w.toList.head hnil = ⟨(w.toList.head hnil).fst, m'⟩ ∧ m₁ = m₂ * m') ∨
      ¬w.fstIdx = some (w.toList.head hnil).fst ∧ m₁ = m₂

Tactic:
rintro rfl

Goal state after:
case pos.mp
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList = []
m₂ : M (w.toList.head hnil).fst
hw : ⟨(w.toList.head hnil).fst, m₂ * (w.toList.head ⋯).snd⟩ ∉ w.toList.tail
hm1 : ¬m₂ * (w.toList.head ⋯).snd = 1
⊢ (∃ m', w.toList.head hnil = ⟨(w.toList.head hnil).fst, m'⟩ ∧ m₂ * (w.toList.head ⋯).snd = m₂ * m') ∨
    ¬w.fstIdx = some (w.toList.head hnil).fst ∧ m₂ * (w.toList.head ⋯).snd = m₂
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
h : cs.IsReduced ω
hw : cs.wordProd ω ≠ 1
⊢ ω ≠ []

Tactic:
rintro rfl

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
h : cs.IsReduced []
hw : cs.wordProd [] ≠ 1
⊢ False
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
⊢ a • 0 = 0

Tactic:
by simp [qsmul_def]

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case h
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
⊢ ((a + b).num * ↑a.den * ↑b.den * (↑↑s * ↑↑s)) • m =
    ((a.num * ↑b.den + b.num * ↑a.den) * ↑(a + b).den * (↑↑s * ↑↑s)) • m

Tactic:
rw [Rat.add_num_den']

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ Finite (Quotient ↑H ↑K) ↔ ∃ I, ⋃ i ∈ I, quotToDoubleCoset H K i = Set.univ

Tactic:
constructor
  · intro _
    cases nonempty_fintype (Quotient (H : Set G) K)
    exact ⟨Finset.univ, by simpa using! iUnion_quotToDoubleCoset _ _⟩
  · rintro ⟨I, hI⟩
    suffices (I : Set (Quotient (H : Set G) K)) = Set.univ by
      simp_rw [← Set.finite_univ_iff, ← this, I.finite_toSet]
    rw [Set.eq_univ_iff_forall] at hI ⊢
    rintro ⟨g⟩
    obtain ⟨_, ⟨i, _, rfl⟩, T, ⟨hi, rfl⟩, hT : g ∈ quotToDoubleCoset H K i⟩ := hI g
    simpa [← (mem_quotToDoubleCoset_iff _ _).mp hT] using! hi

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : DivisibleHull M
ha : 0 < a
b c : ℚ
h : b < c
⊢ 0 < (c - b) • a

Tactic:
qsmul_of_nonneg (sub_pos_of_lt h).le

Goal state after:
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : DivisibleHull M
ha : 0 < a
b c : ℚ
h : b < c
⊢ 0 < ⟨c - b, ⋯⟩ • a
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
x : DivisibleHull M
x✝³ x✝² : M
x✝¹ x✝ : ℕ+
h : ArchimedeanClass.mk (mk x✝³ x✝¹) = ArchimedeanClass.mk (mk x✝² x✝)
⊢ (archimedeanClassOrderHom M) (ArchimedeanClass.mk x✝³) = (archimedeanClassOrderHom M) (ArchimedeanClass.mk x✝²)

Tactic:
simpa [aux_archimedeanClassMk_mk] using h

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case h₂.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a✝ : M
⊢ ((archimedeanClassOrderHomInv M).comp (archimedeanClassOrderHom M)) (ArchimedeanClass.mk a✝) =
    OrderHom.id (ArchimedeanClass.mk a✝)

Tactic:
| mk _
     => 

Goal state after:
case h₂.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a✝ : M
⊢ ((archimedeanClassOrderHomInv M).comp (archimedeanClassOrderHom M)) (ArchimedeanClass.mk a✝) =
    OrderHom.id (ArchimedeanClass.mk a✝)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hne1 : FreeGroup.freeGroupUnitEquivInt.symm n ≠ 1
⊢ n ≠ 0

Tactic:
rintro rfl

Goal state after:
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
hne1 : FreeGroup.freeGroupUnitEquivInt.symm 0 ≠ 1
⊢ False
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
a b : α × Bool
⊢ IsCyclicallyReduced (b :: L ++ [a]) ↔ IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)

Tactic:
isCyclicallyReduced_iff,

Goal state after:
α : Type u
L : List (α × Bool)
a b : α × Bool
⊢ (IsReduced (b :: L ++ [a]) ∧
      ∀ a_1 ∈ (b :: L ++ [a]).getLast?, ∀ b_1 ∈ (b :: L ++ [a]).head?, a_1.1 = b_1.1 → a_1.2 = b_1.2) ↔
    IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
⊢ IsCyclicallyReduced (replicate (n + 1) (head :: tail)).flatten

Tactic:
isCyclicallyReduced_iff,

Goal state after:
α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
⊢ IsReduced (replicate (n + 1) (head :: tail)).flatten ∧
    ∀ a ∈ (replicate (n + 1) (head :: tail)).flatten.getLast?,
      ∀ b ∈ (replicate (n + 1) (head :: tail)).flatten.head?, a.1 = b.1 → a.2 = b.2
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: case cons_append
α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
a✝¹ : α × Bool
l✝ : List (α × Bool)
b✝ : α × Bool
a✝ : IsReduced l✝ → IsCyclicallyReduced (reduceCyclically l✝)
h : IsReduced (a✝¹ :: (l✝ ++ [b✝]))
⊢ IsCyclicallyReduced (reduceCyclically (a✝¹ :: (l✝ ++ [b✝])))

Tactic:
case cons_append a l b ih =>
    rw [reduceCyclically.cons_append]
    split
    case isTrue => exact ih (h.infix ⟨[a], [b], rfl⟩)
    case isFalse h' =>
      rw [isCyclicallyReduced_cons_append_iff]
      exact ⟨h, by simpa using h'⟩

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ mk (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = mk (L₁ ++ (L₂ ++ L₄) ++ L₅)

Tactic:
← mul_mk

Goal state after:
α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ mk (L₁ ++ L₂ ++ invRev L₃) * mk (L₃ ++ L₄ ++ L₅) = mk (L₁ ++ (L₂ ++ L₄) ++ L₅)
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ mk (L₁ ++ L₂ ++ invRev L₃) * mk (L₃ ++ L₄ ++ L₅) = mk (L₁ ++ (L₂ ++ L₄) ++ L₅)

Tactic:
← mul_mk

Goal state after:
α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ mk (L₁ ++ L₂) * mk (invRev L₃) * mk (L₃ ++ L₄ ++ L₅) = mk (L₁ ++ (L₂ ++ L₄) ++ L₅)
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ mk (L₁ ++ L₂) * mk (invRev L₃) * mk (L₃ ++ L₄ ++ L₅) = mk (L₁ ++ (L₂ ++ L₄) ++ L₅)

Tactic:
← mul_mk

Goal state after:
α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ mk L₁ * mk L₂ * mk (invRev L₃) * mk (L₃ ++ L₄ ++ L₅) = mk (L₁ ++ (L₂ ++ L₄) ++ L₅)
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ mk L₁ * mk L₂ * mk (invRev L₃) * mk (L₃ ++ L₄ ++ L₅) = mk (L₁ ++ (L₂ ++ L₄) ++ L₅)

Tactic:
← mul_mk

Goal state after:
α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ mk L₁ * mk L₂ * mk (invRev L₃) * (mk (L₃ ++ L₄) * mk L₅) = mk (L₁ ++ (L₂ ++ L₄) ++ L₅)
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ mk L₁ * mk L₂ * mk (invRev L₃) * (mk (L₃ ++ L₄) * mk L₅) = mk (L₁ ++ (L₂ ++ L₄) ++ L₅)

Tactic:
← mul_mk

Goal state after:
α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ mk L₁ * mk L₂ * mk (invRev L₃) * (mk L₃ * mk L₄ * mk L₅) = mk (L₁ ++ (L₂ ++ L₄) ++ L₅)
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ mk L₁ * mk L₂ * mk (invRev L₃) * (mk L₃ * mk L₄ * mk L₅) = mk (L₁ ++ (L₂ ++ L₄) ++ L₅)

Tactic:
← mul_mk

Goal state after:
α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ mk L₁ * mk L₂ * mk (invRev L₃) * (mk L₃ * mk L₄ * mk L₅) = mk (L₁ ++ (L₂ ++ L₄)) * mk L₅
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ mk L₁ * mk L₂ * mk (invRev L₃) * (mk L₃ * mk L₄ * mk L₅) = mk (L₁ ++ (L₂ ++ L₄)) * mk L₅

Tactic:
← mul_mk

Goal state after:
α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ mk L₁ * mk L₂ * mk (invRev L₃) * (mk L₃ * mk L₄ * mk L₅) = mk L₁ * mk (L₂ ++ L₄) * mk L₅
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ mk L₁ * mk L₂ * mk (invRev L₃) * (mk L₃ * mk L₄ * mk L₅) = mk L₁ * mk (L₂ ++ L₄) * mk L₅

Tactic:
← mul_mk

Goal state after:
α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ mk L₁ * mk L₂ * mk (invRev L₃) * (mk L₃ * mk L₄ * mk L₅) = mk L₁ * (mk L₂ * mk L₄) * mk L₅