mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case inl
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
h✝ : k < m
⊢ x[n + k] = (List.drop n x)[k]

pp: case inl.h
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
h✝ : k < m
⊢ k < (List.drop n x).length

pp: case inl.h
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
h✝ : k < m
⊢ n + k < x.length

Tactic:
List.getElem_drop

Goal state after:
case inl
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
h✝ : k < m
⊢ x[n + k] = x[n + k]

case inl.h
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
h✝ : k < m
⊢ k < (List.drop n x).length

case inl.h
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
h✝ : k < m
⊢ n + k < x.length
Module: Mathlib.Algebra.ContinuedFractions.Translations

Goal state before:
pp: K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : g.s.get? 0 = some gp
⊢ g.dens 1 = gp.b

Tactic:
by simp [den_eq_conts_b, first_cont_eq zeroth_s_eq]

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

Goal state before:
pp: case think
α : Type u
c s' s : Computation α
h : (empty α <|> s.think) = s'
⊢ ((empty α).think <|> s) = (empty α <|> s)

Tactic:
rw [← think_empty]

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

Goal state before:
pp: α : Type u
c s' s : Computation α
h : (empty α <|> s) = s'
⊢ BisimO (fun c₁ c₂ ↦ (empty α <|> c₂) = c₁) (empty α <|> s).destruct s.destruct

Tactic:
induction s using recOn with rw [think_empty]
  | pure s => simp
  | think s => simp only [BisimO, orElse_think, destruct_think]; rw [← think_empty]

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

Goal state before:
pp: case think
α : Type u
c s' s : Computation α
h : (s.think <|> empty α) = s'
⊢ (s <|> (empty α).think) = (s <|> empty α)

Tactic:
rw [← think_empty]

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

Goal state before:
pp: α : Type u
c s' s : Computation α
h : (s <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ ↦ (c₂ <|> empty α) = c₁) (s <|> empty α).destruct s.destruct

Tactic:
induction s using recOn with rw [think_empty]
  | pure s => simp
  | think s => simp only [BisimO, orElse_think, destruct_think]; rw [← think_empty]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
⊢ Option.map₂ g (Option.map f₁ (s₁.get? n)) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) (s₁.get? n) (s₂.get? n)

Tactic:
cases s₁.get? n

Goal state after:
case none
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
⊢ Option.map₂ g (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) none (s₂.get? n)

case some
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val✝ : α
⊢ Option.map₂ g (Option.map f₁ (some val✝)) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) (some val✝) (s₂.get? n)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
⊢ Option.map₂ Prod.mk (Option.map f₁ (s₁.get? n)) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (s₁.get? n) (s₂.get? n))

Tactic:
cases s₁.get? n

Goal state after:
case none
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
⊢ Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none (s₂.get? n))

case some
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val✝ : α
⊢ Option.map₂ Prod.mk (Option.map f₁ (some val✝)) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val✝) (s₂.get? n))
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
x : α
s : Seq α
m n : ℕ
h : m < n
⊢ (s.set m x).drop n = s.drop n

Tactic:
ext1 i
  simp [get?_set_of_ne _ _ (show n + i ≠ m by lia)]

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

Goal state before:
pp: case pos
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
this : ∀ (n : ℕ), b.drop n ≠ nil → motive (a.drop n) (b.drop n)
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
⊢ False

Tactic:
have hb_cons : b.drop (a.length ha) ≠ .nil := by
    intro hb'
    simp only [← length'_eq_zero_iff_nil, drop_length', tsub_eq_zero_iff_le, length'_le_iff] at hb'
    contradiction

Goal state after:
case pos
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
this : ∀ (n : ℕ), b.drop n ≠ nil → motive (a.drop n) (b.drop n)
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
hb_cons : b.drop (a.length ha) ≠ nil
⊢ False
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case zero
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
IH : ∀ m < 0, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ conts, (of v).contsAux 0 = Pair.map Rat.cast conts

pp: case succ.zero
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
IH : ∀ m < 0 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ conts, (of v).contsAux (0 + 1) = Pair.map Rat.cast conts

pp: case succ.succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts

Tactic:
· suffices ∃ gp : Pair ℚ, Pair.mk (1 : K) 0 = gp.map (↑) by simpa [contsAux]
        use Pair.mk 1 0
        simp

Goal state after:
case succ.zero
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
IH : ∀ m < 0 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ conts, (of v).contsAux (0 + 1) = Pair.map Rat.cast conts

case succ.succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries

Goal state before:
pp: case inr
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
⊢ 1 / (B * nB) < ε

Tactic:
have B_ineq : (fib (n + 1) : K) ≤ B :=
      haveI : ¬g.TerminatedAt (n - 1) := mt (terminated_stable n.pred_le) not_terminatedAt_n
      succ_nth_fib_le_of_nth_den (Or.inr this)

Goal state after:
case inr
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
⊢ 1 / (B * nB) < ε
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: 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

Tactic:
have : IntFractPair.of q = ifp_zero := by injection stream_zero_eq

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

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
ifp_n ifp_succ_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ ↑ifp_succ_n.b ≤ ifp_n.fr⁻¹

Tactic:
by
  suffices (⌊ifp_n.fr⁻¹⌋ : K) ≤ ifp_n.fr⁻¹ by
    obtain ⟨_, ifp_n_fr⟩ := ifp_n
    have : ifp_n_fr ≠ 0 := by
      intro h
      simp [h, IntFractPair.stream, nth_stream_eq] at succ_nth_stream_eq
    have : IntFractPair.of ifp_n_fr⁻¹ = ifp_succ_n := by
      simpa [this, IntFractPair.stream, nth_stream_eq, Option.coe_def] using succ_nth_stream_eq
    rwa [← this]
  exact floor_le ifp_n.fr⁻¹

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

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

Tactic:
simp [hb]

Goal state after:
Module: Mathlib.Algebra.DirectSum.Idempotents

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
⊢ (decompose V) (∑ i, idempotent V i) = (decompose V) 1

Tactic:
refine DFunLike.ext _ _ fun i ↦ ?_

Goal state after:
R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
i : I
⊢ ((decompose V) (∑ i, idempotent V i)) i = ((decompose V) 1) i
Module: Mathlib.Algebra.CubicDiscriminant

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

Tactic:
simp [hb]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

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

Tactic:
simp [hb]

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

Goal state before:
pp: case inr
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
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
determinant_eq : pA * B - pB * A = (-1) ^ n
pB_ineq : ↑(fib n) ≤ pB
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
⊢ n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2)

Tactic:
· exact Or.inr not_terminatedAt_pred_n

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

Tactic:
have : Nonempty {l : ℕ // l ≤ k} := ⟨⟨0, zero_le⟩⟩

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
this : Nonempty { l // ↑l ≤ k }
⊢ x ∈ (f.genEigenspace μ) k ↔ ∃ l, ↑l ≤ k ∧ x ∈ ((f - μ • 1) ^ l).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 : ℕ
hk : 0 < k
⊢ f.HasGenEigenvalue μ k ↔ f.HasEigenvalue μ

Tactic:
simp [hk]

Goal state after:
Module: Mathlib.Algebra.Divisibility.Prod

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Semigroup (G i)
x y : (i : ι) → G i
⊢ (∃ c, ∀ (x_1 : ι), y x_1 = (x * c) x_1) ↔ ∀ (i : ι), ∃ c, y i = x i * c

Tactic:
Classical.skolem

Goal state after:
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Semigroup (G i)
x y : (i : ι) → G i
⊢ (∃ c, ∀ (x_1 : ι), y x_1 = (x * c) x_1) ↔ ∃ f, ∀ (x_1 : ι), y x_1 = x x_1 * f x_1
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ((toMatrix c c) ((f ∘ₗ id) ∘ₗ id)).trace = ((toMatrix c c) f).trace

Tactic:
rw [LinearMap.comp_id, LinearMap.comp_id]

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : IsProj p f
inst✝³ : Free R ↥p
inst✝² : Module.Finite R ↥p
inst✝¹ : Free R ↥f.ker
inst✝ : Module.Finite R ↥f.ker
⊢ (LinearMap.trace R M) f = ↑(finrank R ↥p)

Tactic:
h.eq_conj_prodMap,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : IsProj p f
inst✝³ : Free R ↥p
inst✝² : Module.Finite R ↥p
inst✝¹ : Free R ↥f.ker
inst✝ : Module.Finite R ↥f.ker
⊢ (LinearMap.trace R M) ((p.prodEquivOfIsCompl f.ker ⋯).conj (id.prodMap 0)) = ↑(finrank R ↥p)
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
inst✝⁴ : IsDomain R
inst✝³ : IsTorsionFree R M
L : Type u_1
F : Type u_2
inst✝² : SMul R L
inst✝¹ : FunLike F L (End R M)
inst✝ : MulActionHomClass F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
t : R
x : L
⊢ μ (t • x) = t • μ x

Tactic:
by_contra contra
  let g : L → Submodule R M := fun x ↦ (f x).genEigenspace (μ x) k
  have : ⨅ x, g x ≤ g x ⊓ g (t • x) := le_inf_iff.mpr ⟨iInf_le g x, iInf_le g (t • x)⟩
  refine h_ne <| eq_bot_iff.mpr (le_trans this (disjoint_iff_inf_le.mp ?_))
  apply Disjoint.mono_left (genEigenspace_le_smul (f x) (μ x) t k)
  simp only [g, map_smul]
  exact disjoint_genEigenspace (t • f x) (Ne.symm contra) k k

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

Goal state before:
pp: α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
⊢ reduce L = L

Tactic:
by
  rw [← h.red_iff_eq]
  exact reduce.red

Goal state after:
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✝ : AddCommGroupWithOne R
n : ℕ
⊢ ↑↑(Int.negSucc n) = -↑(n + 1)

Tactic:
change coe _ = -coe _

Goal state after:
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✝ : AddCommGroupWithOne R
n : ℕ
⊢ ↑↑(Int.negSucc n) = -↑↑(n + 1)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
A : Type v
inst✝ : CommSemiring A
φ : R →+* A
n✝ : ℕ
hn : n✝ < (Polynomial.map φ f).natDegree
⊢ (Polynomial.map φ f).coeff n✝ ∈ Ideal.map φ 𝓟

Tactic:
rw [coeff_map]

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
A : Type v
inst✝ : CommSemiring A
φ : R →+* A
n✝ : ℕ
hn : n✝ < (Polynomial.map φ f).natDegree
⊢ φ (f.coeff n✝) ∈ Ideal.map φ 𝓟
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case refine_2
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 : U
⊢ IsIntegral R x ↔ ∃ y, (algebraMap S U) y = x

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Goal state after:
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 : U
h : IsIntegral R x
⊢ ∃ y, (algebraMap S U) y = x

case refine_2.refine_2
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 : U
⊢ (∃ y, (algebraMap S U) y = x) → IsIntegral R x
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
x : R
⊢ (↑x * star ↑x).re = x ^ 2

Tactic:
star_coe,

Goal state after:
R : Type u_3
inst✝ : CommRing R
x : R
⊢ (↑x * ↑x).re = x ^ 2
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:
by
  simp_rw [← coe_subset]
  push_cast
  exact Set.smul_set_subset_iff_subset_inv_smul_set

Goal state after:
Module: Mathlib.Algebra.Group.Ideal

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
s : Set M
x : M
⊢ x ∈ closure s ↔ x ∈ s ∨ ∃ y, ∃ z ∈ s, y * z = x

Tactic:
rw [← SetLike.mem_coe, coe_closure]
  simp [mem_mul]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : Mul α
inst✝⁴ : Preorder α
inst✝³ : DecidableEq α
inst✝² : MulLeftMono α
inst✝¹ : MulRightMono α
inst✝ : LocallyFiniteOrderTop α
a b : α
⊢ ↑(Ici a * Ici b) ⊆ ↑(Ici (a * b))

Tactic:
simpa using Set.Ici_mul_Ici_subset' _ _

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Set G
⊢ Nat.card ↑(s / t) ≤ Nat.card ↑s * Nat.card ↑t

Tactic:
rw [div_eq_mul_inv, ← natCard_inv t]

Goal state after:
G : Type u_1
inst✝ : Group G
s t : Set G
⊢ Nat.card ↑(s * t⁻¹) ≤ Nat.card ↑s * Nat.card ↑t⁻¹
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a : G
f : G → α
x✝ : G
⊢ τ a f x✝ = (DomAddAct.mk (-a) +ᵥ f) x✝

Tactic:
simp [DomAddAct.vadd_apply, sub_eq_neg_add]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
f : Set (Submonoid M)
hf : ∀ s ∈ f, s.MulSaturated
x✝¹ x✝ : M
hxy : ∀ p ∈ f, x✝¹ * x✝ ∈ p
⊢ (∀ p ∈ f, x✝¹ ∈ p) ∧ ∀ p ∈ f, x✝ ∈ p

Tactic:
exact ⟨fun s hs ↦ (hf s hs <| hxy s hs).1, fun s hs ↦ (hf s hs <| hxy s hs).2⟩

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

Goal state before:
pp: ι : Type u_1
G : Type u_3
inst✝¹ : CommGroup G
inst✝ : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
k : ι
hk : v k = v i / v j
hk' : k ∈ t
x✝ : i ∈ t
⊢ v i = v k * v j

Tactic:
simp [hk]

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✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
i : ι
hi : f (v i) ≠ 1
hi' : v i⁻¹ = (v i)⁻¹
⊢ v i ∈ Submonoid.closure (v '' baseOf v f) ∨ (v i)⁻¹ ∈ Submonoid.closure (v '' baseOf v f)

Tactic:
rw [Submonoid.closure_image_isMulIndecomposable_baseOf v f]

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
i : ι
hi : f (v i) ≠ 1
hi' : v i⁻¹ = (v i)⁻¹
⊢ v i ∈ Submonoid.closure (v '' {i | 1 < f (v i)}) ∨ (v i)⁻¹ ∈ Submonoid.closure (v '' {i | 1 < f (v i)})
Module: Mathlib.Algebra.GroupWithZero.Torsion

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
this : n • normalizedFactors x = n • normalizedFactors y
⊢ Associated x y

Tactic:
nsmul_right_inj hn,

Goal state after:
M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
this : normalizedFactors x = normalizedFactors y
⊢ Associated x y
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X Y : FintypeCat
f : X ⟶ Y
x : (uSwitch.obj X).obj
⊢ (ConcreteCategory.hom f) ((Fintype.equivFin X.obj).symm x.down) =
    (Fintype.equivFin Y.obj).symm
      ((ConcreteCategory.hom
            (homMk
              (ULift.up ∘
                ⇑(Fintype.equivFin Y.obj) ∘
                  ⇑(ConcreteCategory.hom f.hom) ∘ ⇑(Fintype.equivFin X.obj).symm ∘ ULift.down)))
          x).down

Tactic:
homMk_apply

Goal state after:
X Y : FintypeCat
f : X ⟶ Y
x : (uSwitch.obj X).obj
⊢ (ConcreteCategory.hom f) ((Fintype.equivFin X.obj).symm x.down) =
    (Fintype.equivFin Y.obj).symm
      ((ULift.up ∘
            ⇑(Fintype.equivFin Y.obj) ∘ ⇑(ConcreteCategory.hom f.hom) ∘ ⇑(Fintype.equivFin X.obj).symm ∘ ULift.down)
          x).down
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ (kernelSubobject (X.δ i.succ.succ)).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫
      (kernelSubobject (X.δ i.succ.succ)).arrow ≫ X.δ i.succ.succ ≫ X.δ 0 =
    0

Tactic:
kernelSubobject_arrow_comp_assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ (kernelSubobject (X.δ i.succ.succ)).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫
      0 ≫ X.δ 0 =
    0
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 : SimplicialObject C
⊢ (kernelSubobject (X.δ (Fin.succ 0))).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫
      (kernelSubobject (X.δ (Fin.succ 0))).arrow ≫ X.δ (Fin.succ 0) ≫ X.δ 0 ≫ inv ⊤.arrow =
    0

Tactic:
kernelSubobject_arrow_comp_assoc,

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ (kernelSubobject (X.δ (Fin.succ 0))).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫
      0 ≫ X.δ 0 ≫ inv ⊤.arrow =
    0
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 : SimplicialObject C
n : ℕ
⊢ (kernelSubobject (X.δ (Fin.succ 0))).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫
      (kernelSubobject (X.δ (Fin.succ 0))).arrow ≫ X.δ (Fin.succ 0) ≫ X.δ 0 =
    0

Tactic:
kernelSubobject_arrow_comp_assoc,

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ (kernelSubobject (X.δ (Fin.succ 0))).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫
      0 ≫ X.δ 0 =
    0