mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
⊢ Function.Injective fun S ↦ S.carrier

Tactic:
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩

Goal state after:
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
toSubsemiring✝¹ : Subsemiring L
algebraMap_mem'✝¹ : ∀ (r : K), (algebraMap K L) r ∈ toSubsemiring✝¹.carrier
inv_mem'✝¹ :
  ∀ x ∈ { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹ }.carrier,
    x⁻¹ ∈ { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹ }.carrier
toSubsemiring✝ : Subsemiring L
algebraMap_mem'✝ : ∀ (r : K), (algebraMap K L) r ∈ toSubsemiring✝.carrier
inv_mem'✝ :
  ∀ x ∈ { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }.carrier,
    x⁻¹ ∈ { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }.carrier
⊢ (fun S ↦ S.carrier)
        { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹, inv_mem' := inv_mem'✝¹ } =
      (fun S ↦ S.carrier)
        { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝, inv_mem' := inv_mem'✝ } →
    { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹, inv_mem' := inv_mem'✝¹ } =
      { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝, inv_mem' := inv_mem'✝ }
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: case pos
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField ↥S
x : L
hx : x ∈ S
hx0 : x = 0
⊢ x⁻¹ ∈ S

pp: case neg
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField ↥S
x : L
hx : x ∈ S
hx0 : ¬x = 0
⊢ x⁻¹ ∈ S

Tactic:
· rw [hx0, inv_zero]
      exact S.zero_mem

Goal state after:
case neg
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField ↥S
x : L
hx : x ∈ S
hx0 : ¬x = 0
⊢ x⁻¹ ∈ S
Module: Mathlib.Algebra.CharP.Quotient

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0

Tactic:
let : Fintype (R ⧸ I) := @Fintype.ofFinite _ hq

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
this : Fintype (R ⧸ I) := Fintype.ofFinite (R ⧸ I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑⋯.unit = 1

Tactic:
IsUnit.unit_spec (PNat.isUnit_natCast 1)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑↑1 = 1
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsDomain R
h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_pos : p ≠ 0
p_char : CharP R p
⊢ P

Tactic:
have p_prime : Nat.Prime p := or_iff_not_imp_right.mp (CharP.char_is_prime_or_zero R p) p_pos

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsDomain R
h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_pos : p ≠ 0
p_char : CharP R p
p_prime : Nat.Prime p
⊢ P
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case some
α : Type u
s : Seq α
a : α
s' : Seq α
a' : α
f0 : s.get? 0 = some a'
h : (fun a' ↦ (a', s.tail)) <$> some a' = some (a, s')
⊢ s = cons a s'

Tactic:
· obtain ⟨f, al⟩ := s
    injections _ h1 h2
    rw [← h2]
    apply Subtype.ext
    dsimp [tail, cons]
    rw [h1] at f0
    rw [← f0]
    exact (Stream'.eta f).symm

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

Goal state before:
pp: α : Type u
β : Type v
f : β → Option (α × β)
b : β
⊢ (corec f b).destruct = omap (corec f) (f b)

Tactic:
dsimp [corec, destruct, get]
  rw [show Stream'.corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).1 from rfl]
  dsimp [Corec.f]
  rcases h : f b with - | s; · rfl
  obtain ⟨a, b'⟩ := s; dsimp [Corec.f]
  apply congr_arg fun b' => some (a, b')
  apply Subtype.ext
  dsimp [corec, tail]
  rw [Stream'.corec'_eq, Stream'.tail_cons]
  dsimp [Corec.f]; rw [h]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
s : Stream' α
b : α
x✝ : a ∈ s
n : ℕ
h : (fun b ↦ a = b) (s.get n)
⊢ (fun b ↦ a = b) ((b :: s).tail.get n)

Tactic:
tail_cons,

Goal state after:
α : Type u
a : α
s : Stream' α
b : α
x✝ : a ∈ s
n : ℕ
h : (fun b ↦ a = b) (s.get n)
⊢ (fun b ↦ a = b) (s.get n)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Stream' α
⊢ map f s = f s.head :: map f s.tail

Tactic:
by
  rw [← Stream'.eta (map f s), tail_map, head_map]

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

Goal state before:
pp: α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ → s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
⊢ IsBisimulation motive

Tactic:
intro s₁

Goal state after:
α : Type u
s₁✝ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ → s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
s₁ : Seq α
⊢ ∀ ⦃s₂ : Seq α⦄, motive s₁ s₂ → BisimO motive s₁.destruct s₂.destruct
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := ⋯
⊢ ∀ (s₁ s₂ : Seq α),
    motive' s₁ s₂ → s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive' s₁' s₂'

Tactic:
intro s₁

Goal state after:
α : Type u
s₁✝ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ : Seq α
⊢ ∀ (s₂ : Seq α), motive' s₁ s₂ → s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive' s₁' s₂'
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), (unfolds head tail s).get n = s.get n
s : Stream' α
⊢ (s.head :: unfolds head tail s.tail).tail.get n = s.tail.get n

Tactic:
tail_cons,

Goal state after:
case succ
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), (unfolds head tail s).get n = s.get n
s : Stream' α
⊢ (unfolds head tail s.tail).get n = s.tail.get n
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case h_1
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b✝ : β
a' : α
b : β
h :
  (match Sum.inr b with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)).fst =
    some a'
x✝ : α ⊕ β
a✝ : α
heq✝ :
  (match Sum.inr b with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)).snd =
    Sum.inl a✝
⊢ (some a✝, Sum.inl a✝).fst = some a'

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)).tail.tail.get (2 * n) = s₁.get n.succ

Tactic:
tail_cons,

Goal state after:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₂.head :: (s₁.tail ⋈ s₂.tail)).tail.get (2 * n) = s₁.get n.succ
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case h_2
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b✝ : β
a' : α
b : β
h :
  (match Sum.inr b with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)).fst =
    some a'
x✝ : α ⊕ β
val✝ : β
heq✝ :
  (match Sum.inr b with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)).snd =
    Sum.inr val✝
⊢ (match f val✝ with
        | Sum.inl a => some a
        | Sum.inr val => none,
        f val✝).fst =
    some a'

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)).tail.tail.get (2 * n + 1) = s₂.get n.succ

Tactic:
tail_cons,

Goal state after:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₂.head :: (s₁.tail ⋈ s₂.tail)).tail.get (2 * n + 1) = s₂.get n.succ
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₂.head :: (s₁.tail ⋈ s₂.tail)).tail.get (2 * n + 1) = s₂.get n.succ

Tactic:
tail_cons,

Goal state after:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁.tail ⋈ s₂.tail).get (2 * n + 1) = s₂.get n.succ
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_2.refine_2
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' r' a' : Computation α
r : R r'.think a'.think
h : BisimO R r'.think.destruct a'.think.destruct
⊢ r'.think.head = a'.think.head ∧ R r'.think.tail a'.think.tail

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
l : List α
s : Stream' α
⊢ drop l.length (a :: (l ++ₛ s)).tail = s

Tactic:
tail_cons,

Goal state after:
α : Type u
a : α
l : List α
s : Stream' α
⊢ drop l.length (l ++ₛ s) = s
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
n : ℕ
b : β
⊢ Stream'.map (fun o ↦ Option.casesOn o none (some ∘ f)) s n = some b →
    Stream'.map (fun o ↦ Option.casesOn o none (some ∘ f)) s (n + 1) = some b

Tactic:
by
      dsimp [Stream'.map, Stream'.get]
      rcases e : s n with - | a <;> intro h
      · contradiction
      · rw [al e]; exact h

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.tails.get n = drop n s.tail
s : Stream' α
⊢ (s.tail :: s.tail.tails).tail.get n = drop n s.tail.tail

Tactic:
tail_cons,

Goal state after:
case succ
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.tails.get n = drop n s.tail
s : Stream' α
⊢ s.tail.tails.get n = drop n s.tail.tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
a : α
n : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n
l : List α
s : Stream' α
⊢ a :: (l :: initsCore (l ++ [s.head]) s.tail).tail.get n = (initsCore (a :: l) s).get (n + 1)

Tactic:
tail_cons,

Goal state after:
case succ
α : Type u
a : α
n : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n
l : List α
s : Stream' α
⊢ a :: (initsCore (l ++ [s.head]) s.tail).get n = (initsCore (a :: l) s).get (n + 1)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
s : Stream' α
n✝ : ℕ
⊢ take (n✝ + 1).succ s = ([s.head] :: map (List.cons s.head) s.tail.inits).tail.get n✝

Tactic:
tail_cons,

Goal state after:
case succ
α : Type u
s : Stream' α
n✝ : ℕ
⊢ take (n✝ + 1).succ s = (map (List.cons s.head) s.tail.inits).get n✝
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case some
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
a : α
om : some a ∈ g
h' : f a = b
⊢ ∃ a ∈ ⟨g, al⟩, f a = b

Tactic:
exact ⟨a, om, h'⟩

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

Goal state before:
pp: case zero
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
a : ℤ
⊢ (IntFractPair.of ↑a).fr = 0

Tactic:
simp only [IntFractPair.of, Int.fract_intCast]

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

Goal state before:
pp: case bisim
α : Type u
S T : Seq (Seq1 α)
⊢ IsBisimulation fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)

pp: case r
α : Type u
S T : Seq (Seq1 α)
⊢ ∃ s S_1 T_1,
    (S.append T).join = s.append (S_1.append T_1).join ∧ S.join.append T.join = s.append (S_1.join.append T_1.join)

Tactic:
· rintro s1 s2 ⟨s, S, T, rfl, rfl⟩
    cases s with
    | nil =>
      cases S with
      | nil =>
        cases T with
        | nil => simp
        | cons s T =>
          obtain ⟨a, s⟩ := s
          simpa using ⟨s, nil, T, by simp, by simp⟩
      | cons s S =>
        obtain ⟨a, s⟩ := s
        simpa using ⟨s, S, T, rfl, rfl⟩
    | cons _ s => simpa using ⟨s, S, T, rfl, rfl⟩

Goal state after:
case r
α : Type u
S T : Seq (Seq1 α)
⊢ ∃ s S_1 T_1,
    (S.append T).join = s.append (S_1.append T_1).join ∧ S.join.append T.join = s.append (S_1.join.append T_1.join)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
s : Seq α
n : ℕ
⊢ (s.drop (n + 1)).length' = s.length' - ↑(n + 1)

Tactic:
cases s with
    | nil => simp
    | cons x s =>
      simp only [drop_succ_cons, length'_cons, Nat.cast_add, Nat.cast_one]
      convert! drop_length' using 1
      generalize s.length' = m
      enat_to_nat
      lia

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ fib (n + 2) - fib (n + 1) = fib n

Tactic:
by
  rw [fib_add_two, add_tsub_cancel_right]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ ↑(of q).h = (of v).h

Tactic:
simp_all

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ ↑(of q).h = (of v).h

Tactic:
by
  simp_all

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_1
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
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ (1 - e₂) * ((e' - e' * e₂) * e') = (1 - e₂) * e'

Tactic:
h₂,

Goal state after:
case refine_1
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
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ (1 - e₂) * ((e' - 0) * e') = (1 - e₂) * e'
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_3
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
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ (1 - e₂) * (e' * e₂) = 0

Tactic:
h₂,

Goal state after:
case refine_3
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
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ (1 - e₂) * 0 = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
i j : I
hij : i ≠ j
⊢ IsCoprime (1 - e i) (1 - e j)

Tactic:
exact ⟨1, e i, by simp [mul_sub, he.ortho hij]⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : Nonempty n
I J : RingCon R
eq : matrix n I = matrix n J
r s : R
⊢ I r s ↔ J r s

Tactic:
have := congr_fun (DFunLike.congr_fun eq (Matrix.of fun _ _ ↦ r)) (Matrix.of fun _ _ ↦ s)
    simpa using this

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
c : RingCon R
x y : R
⊢ (matrix n c).ofMatrix x y → c x y

pp: case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
c : RingCon R
x y : R
⊢ c x y → (matrix n c).ofMatrix x y

Tactic:
· intro h
    inhabit n
    simpa using h default default default default

Goal state after:
case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
c : RingCon R
x y : R
⊢ c x y → (matrix n c).ofMatrix x y
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
f : End K V
a b : K
hb : b ≠ 0
⊢ (b • (f - b⁻¹ • a • 1)).ker = (b • f - a • 1).ker

Tactic:
by rw [smul_sub, smul_inv_smul₀ hb]

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
n : ℕ∞
x : M
hk : ↑0 ≤ n
hx : ((f - μ • 1) ^ 0) x = 0
⊢ ((f - μ • 1) ^ 0) (f x) = 0

Tactic:
simp_all

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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
x : M
hx : x ∈ (f.genEigenspace μ₁) k
hx' : x ∈ (f.genEigenspace μ₂) k ⊔ s.sup fun μ ↦ (f.genEigenspace μ) k
this : x ∈ (f.genEigenspace μ₂) k
⊢ x ∈ ⊥

Tactic:
← (f.disjoint_genEigenspace hμ₁₂ k k).eq_bot

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
x : M
hx : x ∈ (f.genEigenspace μ₁) k
hx' : x ∈ (f.genEigenspace μ₂) k ⊔ s.sup fun μ ↦ (f.genEigenspace μ) k
this : x ∈ (f.genEigenspace μ₂) k
⊢ x ∈ (f.genEigenspace μ₁) k ⊓ (f.genEigenspace μ₂) k
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
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ (trace R M) 1 = ↑(finrank R M)

Tactic:
cases subsingleton_or_nontrivial R
  · simp [eq_iff_true_of_subsingleton]
  have b := Module.Free.chooseBasis R M
  rw [trace_eq_matrix_trace R b, toMatrix_one, finrank_eq_card_chooseBasisIndex]
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: K : Type u_6
m : Type u_7
F : Type u_8
inst✝⁴ : Field K
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : FunLike F (Matrix m m K) (Matrix m m K)
inst✝ : AlgHomClass F K (Matrix m m K) (Matrix m m K)
f : F
x : Matrix m m K
⊢ (f x).trace = x.trace

Tactic:
by_cases! Nonempty m

Goal state after:
case pos
K : Type u_6
m : Type u_7
F : Type u_8
inst✝⁴ : Field K
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : FunLike F (Matrix m m K) (Matrix m m K)
inst✝ : AlgHomClass F K (Matrix m m K) (Matrix m m K)
f : F
x : Matrix m m K
h✝ : Nonempty m
⊢ (f x).trace = x.trace

case neg
K : Type u_6
m : Type u_7
F : Type u_8
inst✝⁴ : Field K
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : FunLike F (Matrix m m K) (Matrix m m K)
inst✝ : AlgHomClass F K (Matrix m m K) (Matrix m m K)
f : F
x : Matrix m m K
h✝ : IsEmpty m
⊢ (f x).trace = x.trace
Module: Mathlib.Algebra.Field.GeomSum

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x y : K
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
⊢ ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)

Tactic:
have : x - y ≠ 0 := by simp_all [sub_eq_iff_eq_add]
  rw [← h.geom_sum₂_Ico_mul hmn, mul_div_cancel_right₀ _ this]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : DivisionSemiring α
h : Periodic f c
a : α
⊢ Periodic (fun x ↦ f (x / a)) (c * a)

Tactic:
by simpa only [div_eq_mul_inv] using h.mul_const_inv a

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
m : M₃
hm : i₃ m = 1
⊢ f₃ m = 1

Tactic:
suffices h : i₄ (f₃ m) = 1 by rwa [map_eq_one_iff _ hi₄] at h
    simp [← show g₃ (i₃ m) = i₄ (f₃ m) by simpa using DFunLike.congr_fun hc₃ m, hm]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ Multiplicative.ofAdd (List.countP (fun b ↦ decide (p b)) [x]) =
    if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0

Tactic:
List.countP_singleton,

Goal state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ Multiplicative.ofAdd (if decide (p x) = true then 1 else 0) =
    if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: case coe.ih1
α : Type u_1
x✝ : α
⊢ (lift fun x ↦ ↑(FreeSemigroup.of x)) ((WithOne.lift toFreeMonoid) ↑(FreeSemigroup.of x✝)) = ↑(FreeSemigroup.of x✝)

Tactic:
simp_all

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

Goal state before:
pp: case coe.ih2
α : Type u_1
x✝ : α
y✝ : FreeSemigroup α
a✝¹ : (lift fun x ↦ ↑(FreeSemigroup.of x)) ((WithOne.lift toFreeMonoid) ↑(FreeSemigroup.of x✝)) = ↑(FreeSemigroup.of x✝)
a✝ : (lift fun x ↦ ↑(FreeSemigroup.of x)) ((WithOne.lift toFreeMonoid) ↑y✝) = ↑y✝
⊢ (lift fun x ↦ ↑(FreeSemigroup.of x)) ((WithOne.lift toFreeMonoid) ↑(FreeSemigroup.of x✝ * y✝)) =
    ↑(FreeSemigroup.of x✝ * y✝)

Tactic:
simp_all

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
⊢ IsUnit (C ((algebraMap R K) f.leadingCoeff))

Tactic:
simp_all

Goal state after: