mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: case zero
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
ifp_zero : IntFractPair K
⊢ IntFractPair.stream v 0 = some ifp_zero → v = compExactValue ((of v).contsAux 0) ((of v).contsAux (0 + 1)) ifp_zero.fr

Tactic:
stream_zero_eq

Goal state after:
case zero
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
ifp_zero : IntFractPair K
stream_zero_eq : IntFractPair.stream v 0 = some ifp_zero
⊢ v = compExactValue ((of v).contsAux 0) ((of v).contsAux (0 + 1)) ifp_zero.fr
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ.cons.inl
α : Type u
p : α → Prop
x : α
m : ℕ
ih : ∀ {s : Seq α}, (∀ x ∈ s, p x) → x ∈ take m s → p x
tl : Seq α
h_all : p x ∧ ∀ a ∈ tl, p a
⊢ p x

pp: case succ.cons.inr
α : Type u
p : α → Prop
x : α
m : ℕ
ih : ∀ {s : Seq α}, (∀ x ∈ s, p x) → x ∈ take m s → p x
hd : α
tl : Seq α
h_all : p hd ∧ ∀ a ∈ tl, p a
hx : x ∈ take m tl
⊢ p x

Tactic:
exacts [h_all.left, ih h_all.right hx]

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
i j : ℕ
⊢ i < j → ∀ x ∈ (Seq.cons hd tl).get? i, ∀ y ∈ (Seq.cons hd tl).get? j, R x y

Tactic:
h_ij

Goal state after:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
i j : ℕ
h_ij : i < j
⊢ ∀ x ∈ (Seq.cons hd tl).get? i, ∀ y ∈ (Seq.cons hd tl).get? j, R x y
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
i : ℕ
x : α
hx : x ∈ (Seq.cons hd tl).get? i
y : α
k : ℕ
h_ij : i < k + 1
hy : y ∈ tl.get? k
⊢ R x y

Tactic:
cases i with

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
⊢ i < j → ∀ x ∈ s.get? i, ∀ y ∈ s.get? j, R x y

Tactic:
h_ij

Goal state after:
α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
⊢ ∀ x ∈ s.get? i, ∀ y ∈ s.get? j, R x y
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
R : α → α → Prop
inst✝ : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
h_succ : ∀ {n : ℕ} {x y : α}, s.get? n = some x → s.get? (n + 1) = some y → R x y
i j : ℕ
⊢ i < j → ∀ x ∈ s.get? i, ∀ y ∈ s.get? j, R x y

Tactic:
h_ij

Goal state after:
α : Type u
R : α → α → Prop
inst✝ : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
h_succ : ∀ {n : ℕ} {x y : α}, s.get? n = some x → s.get? (n + 1) = some y → R x y
i j : ℕ
h_ij : i < j
⊢ ∀ x ∈ s.get? i, ∀ y ∈ s.get? j, R x y
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
x✝ : Option (Pair K)
s_succ_succ_nth_eq : s.get? (n + 2) = x✝
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n

Tactic:
cases s_succ_succ_nth_eq : s.get? (n + 2) with

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case zero
q : ℚ
n : ℕ
ifp_zero : IntFractPair ℚ
⊢ IntFractPair.stream q 0 = some ifp_zero → ifp_zero.fr.num ≤ (IntFractPair.of q).fr.num - ↑0

Tactic:
stream_zero_eq

Goal state after:
case zero
q : ℚ
n : ℕ
ifp_zero : IntFractPair ℚ
stream_zero_eq : IntFractPair.stream q 0 = some ifp_zero
⊢ ifp_zero.fr.num ≤ (IntFractPair.of q).fr.num - ↑0
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case inr
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ g.convs (n + 1) = (g.squashGCF n).convs n

Tactic:
obtain ⟨⟨a, b⟩, s_nth_eq⟩ : ∃ gp_n, g.s.get? n = some gp_n :=
      Option.ne_none_iff_exists'.mp not_terminatedAt_n
    have b_ne_zero : b ≠ 0 := nth_partDen_ne_zero (partDen_eq_s_b s_nth_eq)
    cases n with
    | zero =>
      suffices (b * g.h + a) / b = g.h + a / b by
        simpa [squashGCF, s_nth_eq, conv_eq_conts_a_div_conts_b,
          conts_recurrenceAux s_nth_eq zeroth_contAux_eq_one_zero first_contAux_eq_h_one]
      grind
    | succ n' =>
      obtain ⟨⟨pa, pb⟩, s_n'th_eq⟩ : ∃ gp_n', g.s.get? n' = some gp_n' :=
        g.s.ge_stable n'.le_succ s_nth_eq
      -- Notations
      let g' := squashGCF g (n' + 1)
      set pred_conts := g.contsAux (n' + 1) with succ_n'th_contsAux_eq
      set ppred_conts := g.contsAux n' with n'th_contsAux_eq
      let pA := pred_conts.a
      let pB := pred_conts.b
      let ppA := ppred_conts.a
      let ppB := ppred_conts.b
      set pred_conts' := g'.contsAux (n' + 1) with succ_n'th_contsAux_eq'
      set ppred_conts' := g'.contsAux n' with n'th_contsAux_eq'
      let pA' := pred_conts'.a
      let pB' := pred_conts'.b
      let ppA' := ppred_conts'.a
      let ppB' := ppred_conts'.b
      -- first compute the convergent of the squashed gcf
      have : g'.convs (n' + 1) =
          ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB') := by
        have : g'.s.get? n' = some ⟨pa, pb + a / b⟩ :=
          squashSeq_nth_of_not_terminated s_n'th_eq s_nth_eq
        rw [conv_eq_conts_a_div_conts_b,
          conts_recurrenceAux this n'th_contsAux_eq'.symm succ_n'th_contsAux_eq'.symm]
      rw [this]
      -- then compute the convergent of the original gcf by recursively unfolding the continuants
      -- computation twice
      have : g.convs (n' + 2) =
          (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB) := by
        -- use the recurrence once
        have : g.contsAux (n' + 2) = ⟨pb * pA + pa * ppA, pb * pB + pa * ppB⟩ :=
          contsAux_recurrence s_n'th_eq n'th_contsAux_eq.symm succ_n'th_contsAux_eq.symm
        -- and a second time
        rw [conv_eq_conts_a_div_conts_b,
          conts_recurrenceAux s_nth_eq succ_n'th_contsAux_eq.symm this]
      rw [this]
      suffices
        ((pb + a / b) * pA + pa * ppA) / ((pb + a / b) * pB + pa * ppB) =
          (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB) by
        obtain ⟨eq1, eq2, eq3, eq4⟩ : pA' = pA ∧ pB' = pB ∧ ppA' = ppA ∧ ppB' = ppB := by
          simp [*, g', pA, pB, ppA, ppB, pA', pB', ppA', ppB',
            (contsAux_eq_contsAux_squashGCF_of_le <| le_refl <| n' + 1).symm,
            (contsAux_eq_contsAux_squashGCF_of_le n'.le_succ).symm]
        symm
        simpa only [eq1, eq2, eq3, eq4, mul_div_cancel_right₀ _ b_ne_zero]
      grind

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ P.toPoly = C P.d

Tactic:
by
  rw [of_b_eq_zero ha hb, hc, C_0, zero_mul, zero_add]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
hd : P.d = 0
⊢ P.toPoly = 0

Tactic:
of_c_eq_zero ha hb hc,

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
hd : P.d = 0
⊢ C P.d = 0
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
c d : R
inst✝ : Semiring R
hc : c ≠ 0
⊢ { a := 0, b := 0, c := c, d := d }.toPoly.leadingCoeff = c

Tactic:
by
  simp [hc]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ P.toPoly.leadingCoeff = P.d

Tactic:
of_c_eq_zero ha hb hc,

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ (C P.d).leadingCoeff = P.d
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
c d : R
inst✝ : Semiring R
hc : c ≠ 0
⊢ { a := 0, b := 0, c := c, d := d }.toPoly.degree = 1

Tactic:
by
  simp [hc]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
hd : P.d ≠ 0
⊢ P.toPoly.degree = 0

Tactic:
of_c_eq_zero ha hb hc,

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
hd : P.d ≠ 0
⊢ (C P.d).degree = 0
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
c d : R
inst✝ : Semiring R
hc : c ≠ 0
⊢ { a := 0, b := 0, c := c, d := d }.toPoly.natDegree = 1

Tactic:
by
  simp [hc]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ P.toPoly.natDegree = 0

Tactic:
of_c_eq_zero ha hb hc,

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ (C P.d).natDegree = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ Function.Injective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i}))

Tactic:
injective_iff_map_eq_zero

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ ∀ (a : R), (RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) a = 0 → a = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
hμ : f.HasUnifEigenvalue μ 1
h_unit : IsUnit ((algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
v : M
hv : f.HasUnifEigenvector μ 1 v
⊢ μ • v - f v = 0

Tactic:
rw [hv.apply_eq_smul, sub_self]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
l : ℕ
hx : x ∈ ((f - μ • 1) ^ l).ker
⊢ x ∈ ⊥

Tactic:
rwa [LinearMap.ker_eq_bot.mpr] at hx

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
l : ℕ
hx : x ∈ ((f - μ • 1) ^ l).ker
⊢ Function.Injective ⇑((f - μ • 1) ^ l)
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
n : ℕ
⊢ (x ^ n).toWord = reduce (List.replicate n x.toWord).flatten

Tactic:
by
  rw [← mk_toWord (x := x)]
  simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
⊢ #(FreeAbelianGroup α) = max #α ℵ₀

Tactic:
by
  rw [Cardinal.mk_congr (FreeAbelianGroup.equivFinsupp α).toEquiv]
  simp

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
h : (↑s).Pairwise (Function.onFun Nat.Coprime f)
⊢ s.lcm f = s.prod f

Tactic:
rw [show Nat.Coprime = IsRelPrime by ext; exact Nat.coprime_iff_isRelPrime] at h
  exact associated_lcm_prod h |>.eq_of_normalized (normalize_eq _) (normalize_eq _)

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.IntegrallyClosed

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : GCDMonoid R
M : Submonoid R
inst✝ : IsLocalization M A
z : A
⊢ ∃ a b, IsUnit (gcd a b) ∧ z * (algebraMap R A) b = (algebraMap R A) a

Tactic:
obtain ⟨x, ⟨y, hy⟩, rfl⟩ := IsLocalization.exists_mk'_eq M z

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : GCDMonoid R
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
⊢ ∃ a b, IsUnit (gcd a b) ∧ mk' A x ⟨y, hy⟩ * (algebraMap R A) b = (algebraMap R A) a
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case refine_2.refine_1
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : CommRing U
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra S T
inst✝⁶ : Algebra R U
inst✝⁵ : Algebra S U
inst✝⁴ : Algebra T U
inst✝³ : IsScalarTower S T U
inst✝² : IsScalarTower R T U
inst✝¹ : IsIntegralClosure S R T
inst✝ : IsIntegrallyClosedIn T U
x : S
h : IsIntegral R ((algebraMap S T) x)
⊢ ∃ y, (algebraMap S U) y = (algebraMap T U) ((algebraMap S T) x)

Tactic:
exact ⟨x, IsScalarTower.algebraMap_apply ..⟩

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : (algebraMap R K) a ≠ 0
y : K := (algebraMap R K) b / (algebraMap R K) a
⊢ (algebraMap R K) b ^ n / (algebraMap R K) a ^ n - (algebraMap R K) x = 0

Tactic:
replace hx := congr_arg (algebraMap R K) hx

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
K : Type u_1 := FractionRing R
ha : (algebraMap R K) a ≠ 0
y : K := (algebraMap R K) b / (algebraMap R K) a
hx : (algebraMap R K) (b ^ n) = (algebraMap R K) (a ^ n * x)
⊢ (algebraMap R K) b ^ n / (algebraMap R K) a ^ n - (algebraMap R K) x = 0
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ Commute (star a) a

Tactic:
by
    rw [commute_iff_eq, a.star_eq_two_re_sub];
    ext <;> simp <;> ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ normSq a + normSq b + (a * star b + star (a * star b)).re = normSq a + normSq b + 2 * (a * star b).re

Tactic:
self_add_star',

Goal state after:
R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ normSq a + normSq b + (↑(2 * (a * star b).re)).re = normSq a + normSq b + 2 * (a * star b).re
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: case e'_2
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
⊢ (shiftₗ M G h ^ n) f y = ((fwdDiffₗ M G h + 1) ^ n) f y

Tactic:
shiftₗ

Goal state after:
case e'_2
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
⊢ ((fwdDiffₗ M G h + 1) ^ n) f y = ((fwdDiffₗ M G h + 1) ^ n) f y
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: a b : ℤ
⊢ zmultiples a ⊔ zmultiples b = zmultiples ↑(a.gcd b)

Tactic:
by
  simp_rw [← closure_eq_zmultiples, zmultiples_eq_closure, ← closure_union, Set.singleton_union]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
⊢ CommMonoidWithZero α

Tactic:
let _ := e.monoidWithZero

Goal state after:
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := e.monoidWithZero
⊢ CommMonoidWithZero α
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι✝ : Type u_1
G✝ : Type u_3
S✝ : Type u_4
inst✝⁶ : CommGroup G✝
inst✝⁵ : LinearOrder S✝
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp : v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)
hi : v i ∈ closure (v '' s)
x y : G
x✝² : x ∈ closure (v '' s)
x✝¹ : y ∈ closure (v '' s)
hx : x ≠ 1 → 1 < f x
hy : y ≠ 1 → 1 < f y
x✝ : x * y ≠ 1
⊢ 1 < f (x * y)

Tactic:
rcases eq_or_ne x 1 with rfl | hx'

Goal state after:
case inl
ι✝ : Type u_1
G✝ : Type u_3
S✝ : Type u_4
inst✝⁶ : CommGroup G✝
inst✝⁵ : LinearOrder S✝
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp : v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)
hi : v i ∈ closure (v '' s)
y : G
x✝² : y ∈ closure (v '' s)
hy : y ≠ 1 → 1 < f y
x✝¹ : 1 ∈ closure (v '' s)
hx : 1 ≠ 1 → 1 < f 1
x✝ : 1 * y ≠ 1
⊢ 1 < f (1 * y)

case inr
ι✝ : Type u_1
G✝ : Type u_3
S✝ : Type u_4
inst✝⁶ : CommGroup G✝
inst✝⁵ : LinearOrder S✝
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp : v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)
hi : v i ∈ closure (v '' s)
x y : G
x✝² : x ∈ closure (v '' s)
x✝¹ : y ∈ closure (v '' s)
hx : x ≠ 1 → 1 < f x
hy : y ≠ 1 → 1 < f y
x✝ : x * y ≠ 1
hx' : x ≠ 1
⊢ 1 < f (x * y)
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: A B : FintypeCat
⊢ Function.LeftInverse
    (fun i ↦
      { toFun := ⇑(ConcreteCategory.hom i.hom), invFun := ⇑(ConcreteCategory.hom i.inv), left_inv := ⋯,
        right_inv := ⋯ })
    fun e ↦ { hom := homMk ⇑e, inv := homMk ⇑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: A B : FintypeCat
⊢ Function.RightInverse
    (fun i ↦
      { toFun := ⇑(ConcreteCategory.hom i.hom), invFun := ⇑(ConcreteCategory.hom i.inv), left_inv := ⋯,
        right_inv := ⋯ })
    fun e ↦ { hom := homMk ⇑e, inv := homMk ⇑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋1⦌)) ⋯ ≫
      𝟙 (underlying.obj (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ))) ≫
        (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).arrow ≫ Y.δ 0 ≫ inv ⊤.arrow =
    (𝟙 (underlying.obj (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ))) ≫
        (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ inv ⊤.arrow) ≫
      ⊤.factorThru (⊤.arrow ≫ f.app (op ⦋0⦌)) ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
⊢ ((Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋n✝ + 1 + 1⦌)) ⋯ ≫
      if n✝ + 1 + 1 = n✝ + 1 + 1 then
        𝟙 (underlying.obj (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ))) ≫
          (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).factorThru
            ((Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).arrow ≫ Y.δ 0) ⋯
      else 0) =
    (if n✝ + 1 + 1 = n✝ + 1 + 1 then
        𝟙 (underlying.obj (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ))) ≫
          (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
            ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯
      else 0) ≫
      (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋n✝ + 1⦌)) ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ { X := P.X, p := 𝟙 P.X, idem := ⋯ } ⟶ { X := Q.X, p := 𝟙 Q.X, idem := ⋯ }

Tactic:
exact Hom.mk f.f (by simp)

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ ((-1) ^ ↑0 • X.left.δ 0 + (-1) ^ ↑1 • X.left.δ 1) ≫ X.hom.app (op ⦋0⦌) = 0

Tactic:
Fin.val_zero,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ ((-1) ^ 0 • X.left.δ 0 + (-1) ^ ↑1 • X.left.δ 1) ≫ X.hom.app (op ⦋0⦌) = 0
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ ((-1) ^ ↑0 • X.δ 0) =
    NormalizedMooreComplex.objD X i ≫ (NormalizedMooreComplex.objX X i).arrow

Tactic:
Fin.val_zero,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ ((-1) ^ 0 • X.δ 0) =
    NormalizedMooreComplex.objD X i ≫ (NormalizedMooreComplex.objX X i).arrow
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (unop Y✝).rightOpLeftOpIso.hom ≫ f.unop =
    { left := NatTrans.leftOp (NatTrans.rightOp f.unop.op.unop.left), right := f.unop.op.unop.right, w := ⋯ } ≫
      (unop X✝).rightOpLeftOpIso.hom

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case pos
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
hk : ↑k ≤ i
⊢ 0 = ↑(Fin.predAbove 0 ((ConcreteCategory.hom (σ₀Iter i ⋯)) k))

Tactic:
obtain hk | rfl := hk.lt_or_eq

Goal state after:
case pos.inl
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
hk✝ : ↑k ≤ i
hk : ↑k < i
⊢ 0 = ↑(Fin.predAbove 0 ((ConcreteCategory.hom (σ₀Iter i ⋯)) k))

case pos.inr
n m : ℕ
k : Fin (⦋m⦌.len + 1)
h : n + (↑k + 1) = m
hk : ↑k ≤ ↑k
⊢ 0 = ↑(Fin.predAbove 0 ((ConcreteCategory.hom (σ₀Iter ↑k ⋯)) k))
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case pos
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : i < ↑k
⊢ ↑((ConcreteCategory.hom (σ₀Iter i ⋯)) (j.predAbove k)) = ↑k - (i + 1)

Tactic:
Fin.predAbove_of_castSucc_lt _ _ (by grind),

Goal state after:
case pos
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : i < ↑k
⊢ ↑((ConcreteCategory.hom (σ₀Iter i ⋯)) (k.pred ⋯)) = ↑k - (i + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic

Goal state before:
pp: X Y : SSet
y : Y _⦋0⦌
x✝³ x✝² : SimplexCategoryᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : X.obj x✝³
⊢ (ConcreteCategory.hom (Y.map ((Opposite.unop x✝²).const ⦋0⦌ 0).op)) y =
    (ConcreteCategory.hom (Y.map x✝¹)) ((ConcreteCategory.hom (Y.map ((Opposite.unop x✝³).const ⦋0⦌ 0).op)) y)

Tactic:
← CategoryTheory.comp_apply,

Goal state after:
X Y : SSet
y : Y _⦋0⦌
x✝³ x✝² : SimplexCategoryᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : X.obj x✝³
⊢ (ConcreteCategory.hom (Y.map ((Opposite.unop x✝²).const ⦋0⦌ 0).op)) y =
    (ConcreteCategory.hom (Y.map ((Opposite.unop x✝³).const ⦋0⦌ 0).op ≫ Y.map x✝¹)) y
Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic

Goal state before:
pp: X Y Z : SSet
y : Y _⦋0⦌
g : Y ⟶ Z
⊢ const y ≫ g = const ((ConcreteCategory.hom (g.app (Opposite.op ⦋0⦌))) y)

Tactic:
cat_disch

Goal state after: