mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
T : Type u_3
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S T
inst✝⁵ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
f g : A →ₐ[R] B
inst✝ : Module.Flat R T
h₁ : Function.Surjective ⇑(algebraMap S T)
φ : A ⊗[R] S →ₐ[A] A ⊗[R] T := TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T)
ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
  let __spread.0 := TensorProduct.comm R A S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₃ : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] ↥(RingHom.ker (algebraMap S T)) :=
  LinearEquiv.restrictScalars R ((IsScalarTower.toAlgHom R S T).toLinearMap.kerLTensorEquivOfSurjective h₁ A)
e₄' : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T)) :=
  e₃ ≪≫ₗ _root_.TensorProduct.comm R A ↥(RingHom.ker (algebraMap S T)) ≪≫ₗ
        LinearEquiv.restrictScalars R
          (AlgebraTensorModule.cancelBaseChange R S S (↥(RingHom.ker (algebraMap S T))) A).symm ≪≫ₗ
      LinearEquiv.restrictScalars R
        (AlgebraTensorModule.congr (LinearEquiv.refl S ↥(RingHom.ker (algebraMap S T))) ↑ePp.symm) ≪≫ₗ
    LinearEquiv.restrictScalars R (_root_.TensorProduct.comm S (↥(RingHom.ker (algebraMap S T))) (A ⊗[R] S))
r' x : A ⊗[R] S
y : ↥(RingHom.ker (algebraMap S T))
⊢ e₄'.symm (r' • x ⊗ₜ[S] y) = r' • e₄'.symm (x ⊗ₜ[S] y)

Tactic:
| tmul x y =>

Goal state after:
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
⊢ (∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P) → ∀ p > 0, MixedCharZero R p → P

Tactic:
intro h q q_pos q_mixedChar
    rcases q_mixedChar.charP_quotient with ⟨I, hI_ne_top, _⟩
    -- Krull's Thm: There exists a prime ideal `P` such that `I ≤ P`
    rcases Ideal.exists_le_maximal I hI_ne_top with ⟨M, hM_max, h_IM⟩
    let r := ringChar (R ⧸ M)
    have r_pos : r ≠ 0 := by
      have q_zero :=
        congr_arg (Ideal.Quotient.factor h_IM) (CharP.cast_eq_zero (R ⧸ I) q)
      simp only [map_natCast, map_zero] at q_zero
      apply ne_zero_of_dvd_ne_zero (ne_of_gt q_pos)
      exact (CharP.cast_eq_zero_iff (R ⧸ M) r q).mp q_zero
    have r_prime : Nat.Prime r :=
      or_iff_not_imp_right.1 (CharP.char_is_prime_or_zero (R ⧸ M) r) r_pos
    apply h r r_prime
    have : CharZero R := q_mixedChar.toCharZero
    exact ⟨⟨M, hM_max.ne_top, ringChar.of_eq rfl⟩⟩

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a₁✝ : IntermediateField K L
⊢ ∀ ⦃a₂ : IntermediateField K L⦄, a₁✝.toSubalgebra = a₂.toSubalgebra → a₁✝ = a₂

Tactic:
_

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a₁✝ a₂✝ : IntermediateField K L
⊢ a₁✝.toSubalgebra = a₂✝.toSubalgebra → a₁✝ = a₂✝
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a₁✝ : IntermediateField K L
⊢ ∀ ⦃a₂ : IntermediateField K L⦄, a₁✝.toSubfield = a₂.toSubfield → a₁✝ = a₂

Tactic:
_

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a₁✝ a₂✝ : IntermediateField K L
⊢ a₁✝.toSubfield = a₂✝.toSubfield → a₁✝ = a₂✝
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'
f : L →ₐ[K] L'
a₁✝ : IntermediateField K L
⊢ ∀ ⦃a₂ : IntermediateField K L⦄, map f a₁✝ = map f a₂ → a₁✝ = a₂

Tactic:
_

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'
f : L →ₐ[K] L'
a₁✝ a₂✝ : IntermediateField K L
⊢ map f a₁✝ = map f a₂✝ → a₁✝ = a₂✝
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : ¬∃ p > 0, MixedCharZero R p
⊢ P

Tactic:
apply h_equal

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : ¬∃ p > 0, MixedCharZero R p
⊢ Algebra ℚ R
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]

Goal state after:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
⊢ Option.map (fun a' ↦ (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩)) (corec' (Corec.f f) (some b) 0) =
    match f b with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n m : ℕ
s : Stream' α
⊢ drop n (drop m s) = drop (m + n) s

Tactic:
by
  ext; simp [Nat.add_assoc]

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

Goal state before:
pp: α : Type u
x y : α
s t : Stream' α
h : x :: s = y :: t
n : ℕ
⊢ s.get n = t.get n

Tactic:
← get_succ_cons n _ x,

Goal state after:
α : Type u
x y : α
s t : Stream' α
h : x :: s = y :: t
n : ℕ
⊢ (x :: s).get n.succ = t.get n
Module: Mathlib.Data.Seq.Defs

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

Tactic:
_

Goal state after:
case nil.nil
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
r : R nil nil
this✝ : BisimO R nil.destruct nil.destruct
⊢ nil.head = nil.head ∧ R nil.tail nil.tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
f : α → α
a : α
n : ℕ
ih : iterate f (f a) n = map f (iterate f a) n
⊢ f (iterate f (f a) n) = f (iterate f a (n + 1))

Tactic:
rw [map, get] at ih

Goal state after:
case succ
α : Type u
f : α → α
a : α
n : ℕ
ih : iterate f (f a) n = f (iterate f a n)
⊢ f (iterate f (f a) n) = f (iterate f a (n + 1))
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
i✝ : ℕ
⊢ ∀ (h₁ : i✝ < (take n (x ++ₛ a)).length) (h₂ : i✝ < (List.take n x).length),
    (take n (x ++ₛ a))[i✝] = (List.take n x)[i✝]

Tactic:
_

Goal state after:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
i✝ : ℕ
h₁✝ : i✝ < (take n (x ++ₛ a)).length
⊢ ∀ (h₂ : i✝ < (List.take n x).length), (take n (x ++ₛ a))[i✝] = (List.take n x)[i✝]
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
i✝ : ℕ
h₁✝ : i✝ < (take n (x ++ₛ a)).length
⊢ ∀ (h₂ : i✝ < (List.take n x).length), (take n (x ++ₛ a))[i✝] = (List.take n x)[i✝]

Tactic:
_

Goal state after:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
i✝ : ℕ
h₁✝ : i✝ < (take n (x ++ₛ a)).length
h₂✝ : i✝ < (List.take n x).length
⊢ (take n (x ++ₛ a))[i✝] = (List.take n x)[i✝]
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case refine_2
α : Type u
s : Seq α
n : ℕ
hn : ¬s.get? n = none
⊢ ∀ (x : ℕ), s.get? x = none → ∀ m ≤ n, ¬s.get? m = none

Tactic:
_

Goal state after:
case refine_2
α : Type u
s : Seq α
n : ℕ
hn : ¬s.get? n = none
x✝ : ℕ
⊢ s.get? x✝ = none → ∀ m ≤ n, ¬s.get? m = none
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case refine_2
α : Type u
s : Seq α
n : ℕ
hn : ¬s.get? n = none
x✝ : ℕ
⊢ s.get? x✝ = none → ∀ m ≤ n, ¬s.get? m = none

Tactic:
_

Goal state after:
case refine_2
α : Type u
s : Seq α
n : ℕ
hn : ¬s.get? n = none
x✝ : ℕ
h✝ : s.get? x✝ = none
⊢ ∀ m ≤ n, ¬s.get? m = none
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ.some
α : Type u
m : ℕ
ih : ∀ {s : Seq α}, (take m s).length ≤ m
s : Seq α
v : Seq1 α
⊢ (match some v with
      | none => []
      | some (x, r) => x :: take m r).length ≤
    m + 1

Tactic:
obtain ⟨x, r⟩ := v

Goal state after:
case succ.some
α : Type u
m : ℕ
ih : ∀ {s : Seq α}, (take m s).length ≤ m
s : Seq α
x : α
r : Seq α
⊢ (match some (x, r) with
      | none => []
      | some (x, r) => x :: take m r).length ≤
    m + 1
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, s✝.Results a m → (s✝.bind f).Results b (n + m)
⊢ ∀ {m : ℕ}, s✝.think.Results a m → (s✝.think.bind f).Results b (n + m)

Tactic:
_

Goal state after:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, s✝.Results a m → (s✝.bind f).Results b (n + m)
m✝ : ℕ
⊢ s✝.think.Results a m✝ → (s✝.think.bind f).Results b (n + m✝)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case succ.think
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s' : Computation α
h : (s'.bind f).Results b n
a : α
m n' : ℕ
h1 : s'.Results a m
h2 : (f a).Results b n'
e' : n = n' + m
⊢ ∃ a m n_1, s'.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
rw [e']

Goal state after:
case succ.think
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s' : Computation α
h : (s'.bind f).Results b n
a : α
m n' : ℕ
h1 : s'.Results a m
h2 : (f a).Results b n'
e' : n = n' + m
⊢ ∃ a m_1 n, s'.think.Results a m_1 ∧ (f a).Results b n ∧ n' + m + 1 = n + m_1
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
m : a ∈ nil.append s₂
⊢ nil.append s₂ = cons b s' → a ∈ nil ∨ a ∈ s₂

Tactic:
_

Goal state after:
case nil
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
m : a ∈ nil.append s₂
e✝ : nil.append s₂ = cons b s'
⊢ a ∈ nil ∨ a ∈ s₂
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case cons.inl
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
e' : a = c
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
rw [e']

Goal state after:
case cons.inl
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
e' : a = c
⊢ c ∈ cons c t₁ ∨ c ∈ s₂
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f✝ : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f✝ i j hij x) = (g i) x
f'✝ f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst✝ : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g₁ : (i : ι) → G i →+* G' i
g₂ : (i : ι) → G' i →+* G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
i j : ι
h : i ≤ j
⊢ (g₂ j).comp ((g₁ j).comp (f i j h)) = (f'' i j h).comp ((g₂ i).comp (g₁ i))

Tactic:
hg₁ i,

Goal state after:
ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f✝ : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f✝ i j hij x) = (g i) x
f'✝ f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst✝ : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g₁ : (i : ι) → G i →+* G' i
g₂ : (i : ι) → G' i →+* G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
i j : ι
h : i ≤ j
⊢ (g₂ j).comp ((f' i j h).comp (g₁ i)) = (f'' i j h).comp ((g₂ i).comp (g₁ i))
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
a : α
f : α → Seq1 β
⊢ join (f a, nil) = f a

Tactic:
obtain ⟨a, s⟩ := f a

Goal state after:
α : Type u
β : Type v
a✝ : α
f : α → Seq1 β
a : β
s : Seq β
⊢ join ((a, s), nil) = (a, s)
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
⊢ ∃ gp, { a := 1, b := 0 } = Pair.map Rat.cast gp

Tactic:
use Pair.mk 1 0

Goal state after:
case h
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := ⋯
IH : ∀ m < 0, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
⊢ { a := 1, b := 0 } = Pair.map Rat.cast { a := 1, b := 0 }
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
terminatedAt_n : g.TerminatedAt n
g'_eq_g : g' = g
gp✝ : Pair K
⊢ ∀ {m : ℕ}, m < n → g.s.get? m = some gp✝ → 0 < gp✝.a ∧ 0 < gp✝.b

Tactic:
_

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
terminatedAt_n : g.TerminatedAt n
g'_eq_g : g' = g
gp✝ : Pair K
m✝ : ℕ
⊢ m✝ < n → g.s.get? m✝ = some gp✝ → 0 < gp✝.a ∧ 0 < gp✝.b
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: 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)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
⊢ ↑(fib n) + ↑(fib (n + 1)) ≤ ppconts.b + gp.b * pconts.b

Tactic:
have not_terminatedAt_ppred_n : ¬TerminatedAt g (n - 2) :=
          mt (terminated_stable <| Nat.sub_le n 2) not_terminatedAt_n

Goal state after:
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)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
not_terminatedAt_ppred_n : ¬g.TerminatedAt (n - 2)
⊢ ↑(fib n) + ↑(fib (n + 1)) ≤ ppconts.b + gp.b * pconts.b
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
c : ContFract K
n : ℕ
gp : Pair K
m : ℕ
⊢ m < n → (↑↑c).s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b

Tactic:
_

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
c : ContFract K
n : ℕ
gp : Pair K
m : ℕ
a✝ : m < n
⊢ (↑↑c).s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
Module: Mathlib.Algebra.CubicDiscriminant

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

Tactic:
nontriviality R
  rw [Monic, leadingCoeff_of_c_ne_zero ha hb (hc ▸ one_ne_zero), hc]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Cubic R
inst✝² : CommRing R
inst✝¹ : CommRing S
φ : R →+* S
inst✝ : IsDomain S
⊢ (map φ P).roots = (Polynomial.map φ P.toPoly).roots

Tactic:
by
  rw [roots, map_toPoly]

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
⊢ (x - x ^ 2) ^ n ∣
    (x ^ n * ∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) *
      ((1 - x) * ∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1)) ^ n

Tactic:
Commute.mul_pow,

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ (x - x ^ 2) ^ n ∣
    (x ^ n * ∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) *
      ((1 - x) ^ n * (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1)) ^ n)

case h
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (1 - x) (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1))
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝³ : Semifield K
inst✝² : AddCommMonoid V
inst✝¹ : Module K V
inst✝ : Projective K V
f : End K V ≃ₐ[K] End K V
⊢ ∃ a, MulSemiringAction.toAlgEquiv K (End K V) a = f

Tactic:
have ⟨T, hT⟩ := f.eq_linearEquivConjAlgEquiv

Goal state after:
K : Type u_1
V : Type u_2
inst✝³ : Semifield K
inst✝² : AddCommMonoid V
inst✝¹ : Module K V
inst✝ : Projective K V
f : End K V ≃ₐ[K] End K V
T : V ≃ₗ[K] V
hT : f = conjAlgEquiv K T
⊢ ∃ a, MulSemiringAction.toAlgEquiv K (End K V) a = f
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr.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
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
⊢ f (1 - (1 - a ^ n) ^ n) = f e₁

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:
· rcases n with - | n
    · simp at hn
    simp only [map_sub, map_one, map_pow, ha, he₁.pow_succ_eq,
      he₁.one_sub.pow_succ_eq, sub_sub_cancel]

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
⊢ (1 - (1 - a ^ n) ^ n) * e₂ = 0
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : N ∈ I.matrix.carrier
i j k : n
⊢ k ∈ Finset.univ → M i k * N k j ∈ I.toAddSubmonoid

Tactic:
_

Goal state after:
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : N ∈ I.matrix.carrier
i j k : n
a✝ : k ∈ Finset.univ
⊢ M i k * N k j ∈ I.toAddSubmonoid
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matrix n I.jacobson
i : n
⊢ i ∈ Finset.univ → ∑ j, single i j (M i j) ∈ (matrix n I).jacobson

Tactic:
_

Goal state after:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matrix n I.jacobson
i : n
a✝ : i ∈ Finset.univ
⊢ ∑ j, single i j (M i j) ∈ (matrix n I).jacobson
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matrix n I.jacobson
i : n
a✝ : i ∈ Finset.univ
j : n
⊢ j ∈ Finset.univ → single i j (M i j) ∈ (matrix n I).jacobson

Tactic:
_

Goal state after:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matrix n I.jacobson
i : n
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ single i j (M i j) ∈ (matrix n I).jacobson
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i j : I
⊢ j ∈ Finset.univ → j ≠ i → e i * ↑(r j) * e i = 0

Tactic:
_

Goal state after:
R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i j : I
a✝ : j ∈ Finset.univ
⊢ j ≠ i → e i * ↑(r j) * e i = 0
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 : ι
⊢ ((toMatrix b b) ((dualTensorHom R M M) (b.coord i ⊗ₜ[R] b j))).trace = (contractLeft R M) (b.coord i ⊗ₜ[R] b j)

Tactic:
toMatrix_dualTensorHom

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 : ι
⊢ (Matrix.single j i 1).trace = (contractLeft R M) (b.coord i ⊗ₜ[R] b j)
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₄
x : M₂
hm : i₃ (f₂ x) = 1
⊢ g₂ ?m.183 = 1

Tactic:
rwa [show g₂ (i₂ x) = i₃ (f₂ x) by simpa using DFunLike.congr_fun hc₂ x]

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

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
hα : ℵ₀ ≤ #α
⊢ 2 ≤ #α

Tactic:
exact natCast_le_aleph0.trans hα

Goal state after: