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

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this✝ : 1 / den' ≤ 1 / den
this : 0 ≤ pred_conts.b
⊢ 0 < den'

Tactic:
have : 0 < ifp_n.fr⁻¹ :=
          haveI zero_le_ifp_n_fract : 0 ≤ ifp_n.fr :=
            IntFractPair.nth_stream_fr_nonneg stream_nth_eq
          inv_pos.2 (lt_of_le_of_ne zero_le_ifp_n_fract stream_nth_fr_ne_zero.symm)

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this✝¹ : 1 / den' ≤ 1 / den
this✝ : 0 ≤ pred_conts.b
this : 0 < ifp_n.fr⁻¹
⊢ 0 < den'
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this : 1 / den' ≤ 1 / den
⊢ |(-1) ^ n / den'| ≤ 1 / den

Tactic:
have : |(-1) ^ n / den'| = 1 / den' := by
      suffices 1 / |den'| = 1 / den' by rwa [abs_div, abs_neg_one_pow n]
      have : 0 < den' := by
        have : 0 ≤ pred_conts.b :=
          haveI : (fib n : K) ≤ pred_conts.b :=
            haveI : ¬g.TerminatedAt (n - 2) :=
              mt (terminated_stable (n.sub_le 2)) not_terminatedAt_n
            fib_le_of_contsAux_b <| Or.inr this
          le_trans (mod_cast (fib n).zero_le) this
        have : 0 < ifp_n.fr⁻¹ :=
          haveI zero_le_ifp_n_fract : 0 ≤ ifp_n.fr :=
            IntFractPair.nth_stream_fr_nonneg stream_nth_eq
          inv_pos.2 (lt_of_le_of_ne zero_le_ifp_n_fract stream_nth_fr_ne_zero.symm)
        positivity
      rw [abs_of_pos this]

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this✝ : 1 / den' ≤ 1 / den
this : |(-1) ^ n / den'| = 1 / den'
⊢ |(-1) ^ n / den'| ≤ 1 / den
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
⊢ OrthogonalIdempotents (⇑f ∘ e)

Tactic:
classical
  simp [iff_mul_eq, he.mul_eq, ← map_mul f, apply_ite f]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)

Tactic:
have : (x - x ^ 2) ^ n ∣ (1 - (1 - x ^ n) ^ n) - (1 - (1 - x ^ n) ^ n) ^ 2 := by
    conv_rhs => rw [pow_two, ← mul_one_sub, sub_sub_cancel]
    nth_rw 1 3 [← one_pow n]
    rw [← (Commute.one_left x).mul_geom_sum₂, ← (Commute.one_left (1 - x ^ n)).mul_geom_sum₂]
    simp only [sub_sub_cancel, one_pow, one_mul]
    rw [Commute.mul_pow, Commute.mul_mul_mul_comm, ← Commute.mul_pow, mul_one_sub, ← pow_two]
    · exact ⟨_, rfl⟩
    · simp
    · refine .pow_right (.sub_right (.one_right _) (.sum_left _ _ _ fun _ _ ↦ .pow_left ?_ _)) _
      simp
    · exact .sub_left (.one_left _) (.sum_right _ _ _ fun _ _ ↦ .pow_right rfl _)

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
this : (x - x ^ 2) ^ n ∣ 1 - (1 - x ^ n) ^ n - (1 - (1 - x ^ n) ^ n) ^ 2
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
⊢ y = 1 - x → (x * y = 0 ∧ y * x = 0 ↔ IsIdempotentElem x)

Tactic:
rintro rfl

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
⊢ x * (1 - x) = 0 ∧ (1 - x) * x = 0 ↔ IsIdempotentElem x
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 : ℕ
h : f.HasUnifEigenvalue μ ↑k
⊢ k ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
h : f.HasUnifEigenvalue μ ↑0
⊢ False
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
⊢ ↑(f.maxUnifEigenspaceIndex μ) ≤ ↑(finrank K V)

Tactic:
by simpa using maxUnifEigenspaceIndex_le_finrank f μ

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ (trace R M ∘ₗ dualTensorHom R M M) ((b.dualBasis.tensorProduct b) (i, j)) =
    (contractLeft R M) ((b.dualBasis.tensorProduct b) (i, j))

Tactic:
simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]

Goal state after:
case intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ (trace R M) ((dualTensorHom R M M) (b.coord i ⊗ₜ[R] b j)) = (contractLeft R M) (b.coord i ⊗ₜ[R] b j)
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h.right.inr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j).1 + (i, j).2 = l₁ + l₂
hj : l₂ ≤ j
⊢ ((f₁ - μ₁ • 1) ^ i) (((f₂ - μ₂ • 1) ^ j) m) = 0

Tactic:
Module.End.pow_map_zero_of_le hj hl₂,

Goal state after:
case h.right.inr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j).1 + (i, j).2 = l₁ + l₂
hj : l₂ ≤ j
⊢ ((f₁ - μ₁ • 1) ^ i) 0 = 0
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: case refine_3
k : Type u_1
inst✝³ : DivisionRing k
n : ℕ
V : Fin (n + 2) → Type u_2
inst✝² : (i : Fin (n + 2)) → AddCommGroup (V i)
inst✝¹ : (i : Fin (n + 2)) → Module k (V i)
inst✝ : ∀ (i : Fin (n + 2)), FiniteDimensional k (V i)
f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
inj : finrank k ↥(f 0).range = finrank k (V (Fin.castSucc 0))
surj : (f (Fin.last n)).range = ⊤
⊢ ↑(finrank k (V (Fin.last (n + 1)))) = ↑(finrank k ↥(f (Fin.last n)).range)

Tactic:
· #adaptation_note /-- Prior to v4.31.0-rc1, this proof was
      ```
      grind [finrank_top]
      ```
      -/
    rw [surj, finrank_top, Fin.succ_last]

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

Goal state before:
pp: α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : reduce L = L
x₁ : α
x₂ y₂ : Bool
l₁ l₂ : List (α × Bool)
hl : L = l₁ ++ (x₁, x₂) :: ((x₁, x₂).1, y₂) :: l₂
⊢ ((x₁, x₂).1, y₂).2 ≠ !(x₁, x₂).2

Tactic:
rintro rfl

Goal state after:
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : reduce L = L
x₁ : α
x₂ : Bool
l₁ l₂ : List (α × Bool)
hl : L = l₁ ++ (x₁, x₂) :: ((x₁, x₂).1, !(x₁, x₂).2) :: l₂
⊢ False
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: case nil
α : Type u_1
x : α
⊢ ∀ (x : FreeMonoid α), List.foldl (fun x1 x2 ↦ x1 * x2) x (List.map FreeMonoid.of []) = x * ofList []

Tactic:
grind [ofList_nil, ofList_cons]

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: case cons
α : Type u_1
x head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (x : FreeMonoid α), List.foldl (fun x1 x2 ↦ x1 * x2) x (List.map FreeMonoid.of tail✝) = x * ofList tail✝
⊢ ∀ (x : FreeMonoid α),
    List.foldl (fun x1 x2 ↦ x1 * x2) x (List.map FreeMonoid.of (head✝ :: tail✝)) = x * ofList (head✝ :: tail✝)

Tactic:
grind [ofList_nil, ofList_cons]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff * q ^ m + r
⊢ map (algebraMap R K) r = 0

Tactic:
obtain ⟨u, hu⟩ := hf.symm

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff * q ^ m + r
u : K[X]ˣ
hu : map (algebraMap R K) q ^ m * ↑u = map (algebraMap R K) g
⊢ map (algebraMap R K) r = 0
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ⋯
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := ⋯
hg : g = C g.leadingCoeff + r
hr : map (algebraMap R K) r = 0
hm : m = 0
hg' : ¬g.natDegree = 0
⊢ g.leadingCoeff ∈ P

Tactic:
rw [hg, leadingCoeff, coeff_add, ← hg, coeff_C, if_neg hg', zero_add,
    mem_ker, ← coeff_map, hr, coeff_zero]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : x ^ f.natDegree + ∑ i, f.coeff ↑i * x ^ ↑i = 0
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ -∑ i, f.coeff ↑i * x ^ ↑i ∈ 𝓟

Tactic:
neg_mem_iff

Goal state after:
R : Type u
inst✝ : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : x ^ f.natDegree + ∑ i, f.coeff ↑i * x ^ ↑i = 0
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ ∑ i, f.coeff ↑i * x ^ ↑i ∈ 𝓟
Module: Mathlib.Algebra.Group.Action.Equidecomp

Goal state before:
pp: X : Type u_1
G : Type u_2
A B C : Set X
inst✝¹ : Monoid G
inst✝ : MulAction G X
f g : Equidecomp X G
⊢ ∃ S, IsDecompOn (↑(f.trans g.toPartialEquiv)) (f.trans g.toPartialEquiv).source S

Tactic:
classical exact ⟨g.witness * f.witness, g.isDecompOn.comp' f.isDecompOn⟩

Goal state after:
Module: Mathlib.Algebra.Group.Action.Equidecomp

Goal state before:
pp: X : Type u_1
G : Type u_2
A B C : Set X
inst✝¹ : Monoid G
inst✝ : MulAction G X
f g : Equidecomp X G
⊢ ∃ S, IsDecompOn (↑(f.trans g.toPartialEquiv)) (f.trans g.toPartialEquiv).source S

Tactic:
by classical exact ⟨g.witness * f.witness, g.isDecompOn.comp' f.isDecompOn⟩

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
by
  simp only [star_add, ← self_mul_star, mul_add, add_mul, add_assoc, add_left_comm]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ ↑(a • s) ⊆ ↑t ↔ ↑s ⊆ ↑(a⁻¹ • t)

Tactic:
push_cast

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ a • ↑s ⊆ ↑t ↔ ↑s ⊆ a⁻¹ • ↑t
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ ↑s ⊆ ↑(a • t) ↔ ↑(a⁻¹ • s) ⊆ ↑t

Tactic:
push_cast

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ ↑s ⊆ a • ↑t ↔ a⁻¹ • ↑s ⊆ ↑t
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : s.Nonempty
⊢ ↑(s • univ) = ↑univ

Tactic:
push_cast

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : s.Nonempty
⊢ ↑s • Set.univ = Set.univ
Module: Mathlib.Algebra.Group.Pointwise.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝⁵ : Mul α
inst✝⁴ : PartialOrder α
inst✝³ : DecidableEq α
inst✝² : MulLeftStrictMono α
inst✝¹ : MulRightStrictMono α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ ↑(Ico a b * Icc c d) ⊆ ↑(Ico (a * c) (b * d))

Tactic:
simpa using Set.Ico_mul_Icc_subset' _ _ _ _

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: case inv
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
a : ι →₀ ℤ
hx : (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
⊢ ∃ a_1, (a.prod fun x1 x2 ↦ f x1 ^ x2)⁻¹ = a_1.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
use -a

Goal state after:
case h
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
a : ι →₀ ℤ
hx : (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
⊢ (a.prod fun x1 x2 ↦ f x1 ^ x2)⁻¹ = (-a).prod fun x1 x2 ↦ f x1 ^ x2
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
a : α
inst✝ : Fintype β
ha : a ≠ 0
⊢ ↑(a • univ) = ↑univ

Tactic:
push_cast

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
a : α
inst✝ : Fintype β
ha : a ≠ 0
⊢ a • Set.univ = Set.univ
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : s.Nontrivial
⊢ ↑(s • univ) = ↑univ

Tactic:
push_cast

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : s.Nontrivial
⊢ ↑s • Set.univ = Set.univ
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

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

Tactic:
let _ := e.mulZeroOneClass
  let _ := e.pow ℕ
  apply e.injective.monoidWithZero _ <;> intros <;> exact e.apply_symm_apply _

Goal state after:
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
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
s : Set ι
hst : s ⊆ {j | IsMulIndecomposable v {i | 1 < f (v i)} j}
i : ι
⊢ v i ≠ 1

Tactic:
by contrapose! hf; exact ⟨i, by simp [hf]⟩

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝³ : Monoid M
inst✝² : LinearOrder S
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi : v i ∈ closure (v '' {i | 1 < f (v i)})
x y : M
x✝¹ : x ∈ closure (v '' {i | 1 < f (v i)})
x✝ : y ∈ closure (v '' {i | 1 < f (v i)})
hx : x = 1 ∨ 1 < f x
hy : y = 1 ∨ 1 < f y
⊢ x * y = 1 ∨ 1 < f (x * y)

Tactic:
rcases hx with rfl | hx

Goal state after:
case inl
ι : Type u_1
M : Type u_2
S : Type u_4
inst✝³ : Monoid M
inst✝² : LinearOrder S
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi : v i ∈ closure (v '' {i | 1 < f (v i)})
y : M
x✝¹ : y ∈ closure (v '' {i | 1 < f (v i)})
hy : y = 1 ∨ 1 < f y
x✝ : 1 ∈ closure (v '' {i | 1 < f (v i)})
⊢ 1 * y = 1 ∨ 1 < f (1 * y)

case inr
ι : Type u_1
M : Type u_2
S : Type u_4
inst✝³ : Monoid M
inst✝² : LinearOrder S
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi : v i ∈ closure (v '' {i | 1 < f (v i)})
x y : M
x✝¹ : x ∈ closure (v '' {i | 1 < f (v i)})
x✝ : y ∈ closure (v '' {i | 1 < f (v i)})
hy : y = 1 ∨ 1 < f y
hx : 1 < f x
⊢ x * y = 1 ∨ 1 < f (x * y)
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: case mpr
X : FintypeCat
f : X.obj → X.obj
⊢ f = id → homMk f = 𝟙 X

Tactic:
rintro rfl

Goal state after:
case mpr
X : FintypeCat
⊢ homMk id = 𝟙 X
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: case mpr
X Y Z : FintypeCat
f : X.obj → Y.obj
g : Y.obj → Z.obj
h : X.obj → Z.obj
⊢ h = g ∘ f → homMk h = homMk f ≫ homMk g

Tactic:
rintro rfl

Goal state after:
case mpr
X Y Z : FintypeCat
f : X.obj → Y.obj
g : Y.obj → Z.obj
⊢ homMk (g ∘ f) = homMk f ≫ homMk g
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := ⋯
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
a b : ↑Y.1
h : φ b < φ a
this : b ≤ a
⊢ b ≠ a

Tactic:
rintro rfl

Goal state after:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
b : ↑Y.1
h : φ b < φ b
this : b ≤ b
⊢ False
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case refine_1
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
⊢ Monotone φ

Tactic:
intro a b
      contrapose
      intro h
      simp only [not_le] at h ⊢
      suffices b ≤ a by
        apply lt_of_le_of_ne this
        rintro rfl
        exfalso
        simp at h
      have H : f (φ b) ≤ f (φ a) := f.hom.hom.monotone (le_of_lt h)
      simpa only [hφ] using H

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case i_surj.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ j' ≠ 0

Tactic:
rintro rfl

Goal state after:
case i_surj.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i' : Fin (n + 2)
hij' : ↑i' < ↑0
⊢ False
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl.inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : j.castSucc < k
⊢ j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)

Tactic:
· rw [Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hjk),
      Fin.predAbove_of_castSucc_lt _ _ hjk, Fin.succAbove_of_castSucc_lt,
      Fin.castSucc_pred_eq_pred_castSucc]
      rwa [Fin.castSucc_lt_iff_succ_le, Fin.succ_pred]

Goal state after: