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
n : ℕ
IH : ∀ m < n, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n ≤ 1 ∨ ¬(of v).TerminatedAt (n - 2)
⊢ ↑(fib n) ≤ ((of v).contsAux n).b

Tactic:
rcases n with (_ | _ | n)

Goal state after:
case zero
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
IH : ∀ m < 0, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : 0 ≤ 1 ∨ ¬(of v).TerminatedAt (0 - 2)
⊢ ↑(fib 0) ≤ ((of v).contsAux 0).b

case succ.zero
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
IH : ∀ m < 0 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : 0 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (0 + 1 - 2)
⊢ ↑(fib (0 + 1)) ≤ ((of v).contsAux (0 + 1)).b

case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
⊢ ↑(fib (n + 1 + 1)) ≤ ((of v).contsAux (n + 1 + 1)).b
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case inl
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_eq_zero : ifp.fr = 0
⊢ let g := of v;
  let B := (g.contsAux (n + 1)).b;
  let pB := (g.contsAux n).b;
  v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
suffices v - g.convs n = 0 by simpa [ifp_fr_eq_zero]

Goal state after:
case inl
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_eq_zero : ifp.fr = 0
⊢ v - g.convs n = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case none.none
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
ne : none ≠ none
⊢ none.elim x e * none.elim x e = 0

pp: case none.some
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
j : I
ne : none ≠ some j
⊢ none.elim x e * (some j).elim x e = 0

pp: case some.none
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
i : I
ne : some i ≠ none
⊢ (some i).elim x e * none.elim x e = 0

pp: case some.some
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
i j : I
ne : some i ≠ some j
⊢ (some i).elim x e * (some j).elim x e = 0

Tactic:
· cases ne rfl

Goal state after:
case none.some
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
j : I
ne : none ≠ some j
⊢ none.elim x e * (some j).elim x e = 0

case some.none
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
i : I
ne : some i ≠ none
⊢ (some i).elim x e * none.elim x e = 0

case some.some
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
i j : I
ne : some i ≠ some j
⊢ (some i).elim x e * (some j).elim x e = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr.refine_2
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
n : ℕ
hn : (a - a ^ 2) ^ n = 0
⊢ (1 - (1 - a ^ n) ^ n) * e₂ = 0

Tactic:
obtain ⟨k, hk⟩ := (Commute.one_left (MulOpposite.op <| 1 - a ^ n)).sub_dvd_pow_sub_pow n

Goal state after:
case inr.refine_2
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
n : ℕ
hn : (a - a ^ 2) ^ n = 0
k : Rᵐᵒᵖ
hk : 1 ^ n - MulOpposite.op (1 - a ^ n) ^ n = (1 - MulOpposite.op (1 - a ^ n)) * k
⊢ (1 - (1 - a ^ n) ^ n) * e₂ = 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
k : ℕ
x : M
⊢ x ∈ (f.genEigenspace μ) ↑k ↔ x ∈ ((f - μ • 1) ^ k).ker

Tactic:
mem_genEigenspace

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 : ℕ
x : M
⊢ (∃ l, ↑l ≤ ↑k ∧ x ∈ ((f - μ • 1) ^ l).ker) ↔ x ∈ ((f - μ • 1) ^ k).ker
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
hx : x ∈ (f.genEigenspace μ) k
⊢ x ∈ ⊥

Tactic:
mem_genEigenspace

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
hx : ∃ l, ↑l ≤ k ∧ x ∈ ((f - μ • 1) ^ l).ker
⊢ x ∈ ⊥
Module: Mathlib.Algebra.Divisibility.Prod

Goal state before:
pp: G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Semigroup G₁
inst✝ : Semigroup G₂
x y : G₁ × G₂
⊢ x ∣ y ↔ x.1 ∣ y.1 ∧ x.2 ∣ y.2

Tactic:
by
  cases x; cases y
  simp only [dvd_def, Prod.exists, Prod.mk_mul_mk, Prod.mk.injEq,
    exists_and_left, exists_and_right]

Goal state after:
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }
r x : A
⊢ (↑fe).1 (r * x) * (↑fe).2 = (↑fe).1 r * ((↑fe).1 x * (↑fe).2)

Tactic:
rw [map_mul, mul_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
s : Finset M
b : Basis (↥s) R M
⊢ IsNilpotent ((trace R M) f)

Tactic:
trace_eq_matrix_trace R b

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
s : Finset M
b : Basis (↥s) R M
⊢ IsNilpotent ((toMatrix b b) f).trace
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
inst✝ : Free R S
h : finrank R S = 1
⊢ Function.Bijective ⇑(algebraMap R S)

Tactic:
by
  have : Module.Finite R S := finite_of_finrank_pos (by grind)
  have : Free R (Module.End R S) := .of_equiv (dualTensorHomEquiv R S S)
  let f : S →ₐ[R] (S →ₗ[R] S) := Algebra.lmul R S
  have h1 : LinearMap.trace R S ∘ₗ f ∘ₗ Algebra.linearMap R S = LinearMap.id := by ext; simp [h]
  let b : Basis (Unit × Unit) R (End R S) :=
    .map (.tensorProduct (.dualBasis <| basisUnique Unit h) (basisUnique Unit h))
      (dualTensorHomEquiv R S S)
  have h2 : (f ∘ₗ Algebra.linearMap R S) ∘ₗ LinearMap.trace R S = LinearMap.id :=
    b.ext fun i ↦
      (basisUnique Unit h).ext fun j ↦ (by simp [f, b, Basis.tensorProduct])
  let eq : R ≃ₗ[R] End R S := .ofLinearMap (f ∘ₗ Algebra.linearMap R S) (.trace R S) h2 h1
  have hf : Function.Bijective f := ⟨Algebra.lmul_injective, .of_comp eq.surjective⟩
  exact (Function.Bijective.of_comp_iff' hf _).mp eq.bijective

Goal state after:
Module: Mathlib.Algebra.Field.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : NonAssocSemiring α
inst✝ : Ring β
h : Antiperiodic f c
n : ℕ
⊢ f (x + ↑n * c) = (-1) ^ n * f x

Tactic:
simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
    Int.cast_one] using h.add_nsmul_eq n

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β α✝ : Type u
x✝ x y : FreeMagma α✝
ih1 : id <$> x = x
ih2 : id <$> y = y
⊢ id <$> x * id <$> y = x * y

Tactic:
ih1,

Goal state after:
α β α✝ : Type u
x✝ x y : FreeMagma α✝
ih1 : id <$> x = x
ih2 : id <$> y = y
⊢ x * id <$> y = x * y
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β α✝ β✝ γ✝ : Type u
x✝ : FreeMagma α✝
f : α✝ → FreeMagma β✝
g : β✝ → FreeMagma γ✝
x y : FreeMagma α✝
ih1 : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ih2 : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f >>= g) * (y >>= f >>= g) = (x >>= fun x ↦ f x >>= g) * (y >>= fun x ↦ f x >>= g)

Tactic:
ih1,

Goal state after:
α β α✝ β✝ γ✝ : Type u
x✝ : FreeMagma α✝
f : α✝ → FreeMagma β✝
g : β✝ → FreeMagma γ✝
x y : FreeMagma α✝
ih1 : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ih2 : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= fun x ↦ f x >>= g) * (y >>= f >>= g) = (x >>= fun x ↦ f x >>= g) * (y >>= fun x ↦ f x >>= g)
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ : Type u
x✝ x y : FreeMagma α✝
ih1 : traverse pure x = pure x
ih2 : traverse pure y = pure y
⊢ (fun x1 x2 ↦ x1 * x2) <$> traverse pure x <*> traverse pure y = pure (x * y)

Tactic:
ih1,

Goal state after:
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ : Type u
x✝ x y : FreeMagma α✝
ih1 : traverse pure x = pure x
ih2 : traverse pure y = pure y
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure x <*> traverse pure y = pure (x * y)
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x <*>
      traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y =
    Functor.Comp.mk (traverse f <$> traverse g (x * y))

Tactic:
ih1,

Goal state after:
α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> Functor.Comp.mk (traverse f <$> traverse g x) <*>
      traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y =
    Functor.Comp.mk (traverse f <$> traverse g (x * y))
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (pure ∘ f) x = pure (f <$> x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> traverse (pure ∘ f) x <*> traverse (pure ∘ f) y = pure (f <$> (x * y))

Tactic:
ih1,

Goal state after:
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (pure ∘ f) x = pure (f <$> x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure (f <$> x) <*> traverse (pure ∘ f) y = pure (f <$> (x * y))
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β α✝ : Type u
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : id <$> pure x = pure x
ih2 : id <$> y = y
⊢ id <$> pure x * id <$> y = pure x * y

Tactic:
ih1,

Goal state after:
α β α✝ : Type u
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : id <$> pure x = pure x
ih2 : id <$> y = y
⊢ pure x * id <$> y = pure x * y
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β α✝ β✝ γ✝ : Type u
x✝ : FreeSemigroup α✝
g : α✝ → FreeSemigroup β✝
f : β✝ → FreeSemigroup γ✝
x : α✝
y : FreeSemigroup α✝
ih1 : pure x >>= g >>= f = pure x >>= fun x ↦ g x >>= f
ih2 : y >>= g >>= f = y >>= fun x ↦ g x >>= f
⊢ (pure x >>= g >>= f) * (y >>= g >>= f) = (pure x >>= fun x ↦ g x >>= f) * (y >>= fun x ↦ g x >>= f)

Tactic:
ih1,

Goal state after:
α β α✝ β✝ γ✝ : Type u
x✝ : FreeSemigroup α✝
g : α✝ → FreeSemigroup β✝
f : β✝ → FreeSemigroup γ✝
x : α✝
y : FreeSemigroup α✝
ih1 : pure x >>= g >>= f = pure x >>= fun x ↦ g x >>= f
ih2 : y >>= g >>= f = y >>= fun x ↦ g x >>= f
⊢ (pure x >>= fun x ↦ g x >>= f) * (y >>= g >>= f) = (pure x >>= fun x ↦ g x >>= f) * (y >>= fun x ↦ g x >>= f)
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ : Type u
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse pure (of x) = pure (of x)
ih2 : traverse pure y = pure y
⊢ (fun x1 x2 ↦ x1 * x2) <$> traverse pure (of x) <*> traverse pure y = pure (of x * y)

Tactic:
ih1,

Goal state after:
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ : Type u
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse pure (of x) = pure (of x)
ih2 : traverse pure y = pure y
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure (of x) <*> traverse pure y = pure (of x * y)
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x) = Functor.Comp.mk (traverse f <$> traverse g (pure x))
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x) <*>
      traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y =
    Functor.Comp.mk (traverse f <$> traverse g (pure x * y))

Tactic:
ih1,

Goal state after:
α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x) = Functor.Comp.mk (traverse f <$> traverse g (pure x))
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> Functor.Comp.mk (traverse f <$> traverse g (pure x)) <*>
      traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y =
    Functor.Comp.mk (traverse f <$> traverse g (pure x * y))
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (pure ∘ f) (of x) = pure (f <$> of x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> traverse (pure ∘ f) (of x) <*> traverse (pure ∘ f) y = pure (f <$> (of x * y))

Tactic:
ih1,

Goal state after:
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (pure ∘ f) (of x) = pure (f <$> of x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure (f <$> of x) <*> traverse (pure ∘ f) y = pure (f <$> (of x * y))
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
⊢ ∃ m r, g = C g.leadingCoeff * q ^ m + r ∧ map (algebraMap R K) r = 0 ∧ (m = 0 → IsUnit g)

Tactic:
have hgP : g.leadingCoeff ∉ P := by
    simp only [mem_ker, P]
    obtain ⟨h, rfl⟩ := hg_div
    simp only [leadingCoeff_mul, map_mul, ne_eq, mul_eq_zero, not_or] at hf_lC
    exact hf_lC.1

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
⊢ ∃ m r, g = C g.leadingCoeff * q ^ m + r ∧ map (algebraMap R K) r = 0 ∧ (m = 0 → IsUnit g)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: case refine_2
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : (aeval x) f = 0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
y : S
hy : y ∈ R[x]
H : (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
⊢ (algebraMap R S) p * (y * x ^ k) = x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k

Tactic:
· rw [← mul_assoc _ y, H]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this : Algebra S K := g.toAlgebra
⊢ algebraMap R K = (algebraMap S K).comp (algebraMap R S)

Tactic:
rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
n : ℕ
hn : ¬n = f.natDegree
⊢ f.coeff n ∈ P

Tactic:
by_cases hn' : n < f.natDegree

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
n : ℕ
hn : ¬n = f.natDegree
hn' : n < f.natDegree
⊢ f.coeff n ∈ P

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
n : ℕ
hn : ¬n = f.natDegree
hn' : ¬n < f.natDegree
⊢ f.coeff n ∈ P
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ
⊢ ↑↑x✝ = ↑x✝.num / ↑x✝.den

Tactic:
Rat.cast_def,

Goal state after:
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ
⊢ ↑(↑x✝.num / ↑x✝.den) = ↑x✝.num / ↑x✝.den
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: G : Type u_5
H : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
a : G
f : G → H
⊢ support (τ a f) = a +ᵥ support f

Tactic:
ext; simp [mem_vadd_set_iff_neg_vadd_mem, sub_eq_neg_add]

Goal state after:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x ↦ a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x ↦ a₂, monotone' := ⋯ }
⊢ a₁ = a₂

Tactic:
change g₁ (ULift.up (0 : Fin 1)) = g₂ (ULift.up (0 : Fin 1))

Goal state after:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x ↦ a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x ↦ a₂, monotone' := ⋯ }
⊢ (ConcreteCategory.hom g₁) { down := 0 } = (ConcreteCategory.hom g₂) { down := 0 }
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x ↦ a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x ↦ a₂, monotone' := ⋯ }
eq : g₁ = g₂
⊢ (ConcreteCategory.hom g₁) { down := 0 } = (ConcreteCategory.hom g₂) { down := 0 }

Tactic:
eq

Goal state after:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x ↦ a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x ↦ a₂, monotone' := ⋯ }
eq : g₁ = g₂
⊢ (ConcreteCategory.hom g₂) { down := 0 } = (ConcreteCategory.hom g₂) { down := 0 }
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case mp
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
⊢ False

Tactic:
have h : p₁ m = p₂ m := by
      congr
      rw [← cancel_epi f]
      ext a : 3
      simp only [p₁, p₂, hom_hom_comp, OrderHom.comp_coe, Function.comp_apply]
      change ite _ _ _ = ite _ _ _
      split_ifs with h₁ h₂ h₂
      any_goals rfl
      · exfalso
        exact h₂ (le_of_lt h₁)
      · exfalso
        exact hm a (eq_of_le_of_not_lt h₂ h₁)

Goal state after:
case mp
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
h : (ConcreteCategory.hom p₁) m = (ConcreteCategory.hom p₂) m
⊢ False