mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
⊢ ∃ i g', (iP ≫ π) ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i

Tactic:
obtain ⟨c'⟩ := IsFiltered.cocone_nonempty (WidePushoutShape.wideSpan i i' hi')

Goal state after:
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
⊢ ∃ i g', (iP ≫ π) ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: case mp
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
⊢ (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0 → x ∈ Set.range ⇑F

Tactic:
intro H
    obtain ⟨y, hy⟩ := (hπ₁ _).mp H
    obtain ⟨k, hk⟩ : σ (ι₃ x) - f₁ y ∈ Set.range ι₂ := by
      rw [← hι₂, map_sub, ← H₂, ← hy, sub_eq_zero]; exact congr($h₁ y)
    refine ⟨k, h ?_⟩
    rw [← ι₃.comp_apply, ← hF, f₂.comp_apply, hk, map_sub, H₁, hf.apply_apply_eq_zero, sub_zero]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Limits

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
⊢ ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder ≫ f = ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder ≫ g

Tactic:
rw [equalizer_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasFiniteWidePushouts C
⊢ HasFiniteLimits (Under B)ᵒᵖ

Tactic:
exact hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits (Over.opEquivOpUnder _).inverse

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s :
  PullbackCone ((pair (Over.mk f) (Over.mk g)).obj { as := WalkingPair.left }).hom
    ((pair (Over.mk f) (Over.mk g)).obj { as := WalkingPair.right }).hom
⊢ Over.Hom.left (hc.lift (pullbackConeEquivBinaryFan.functor.obj s)) ≫ Over.Hom.left c.fst = s.fst

Tactic:
by simpa only using! congr($(hc.fac _ _).left)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s :
  PullbackCone ((pair (Over.mk f) (Over.mk g)).obj { as := WalkingPair.left }).hom
    ((pair (Over.mk f) (Over.mk g)).obj { as := WalkingPair.right }).hom
⊢ Over.Hom.left (hc.lift (pullbackConeEquivBinaryFan.functor.obj s)) ≫ Over.Hom.left c.snd = s.snd

Tactic:
by simpa only using! congr($(hc.fac _ _).left)

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
⊢ False

Tactic:
rcases exists_prime_addOrderOf_dvd_card p h with ⟨r, hr⟩

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
⊢ False
Module: Mathlib.Algebra.CharP.LocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
⊢ q = 0 ∨ IsPrimePow q

Tactic:
apply or_iff_not_imp_left.2
  intro q_pos
  let K := IsLocalRing.ResidueField R
  have RM_char := ringChar.charP K
  let r := ringChar K
  let n := q.factorization r
  -- `r := char(R/m)` is either prime or zero:
  rcases CharP.char_is_prime_or_zero K r with r_prime | r_zero
  · let a := q / r ^ n
    -- If `r` is prime, we can write `q` as `a * r^n` ...
    have q_eq_a_mul_rn : q = r ^ n * a := by rw [Nat.mul_div_cancel' (Nat.ordProj_dvd q r)]
    have r_ne_dvd_a := Nat.not_dvd_ordCompl r_prime q_pos
    have rn_dvd_q : r ^ n ∣ q := ⟨a, q_eq_a_mul_rn⟩
    rw [mul_comm] at q_eq_a_mul_rn
    -- ... where `a` is a unit.
    have a_unit : IsUnit (a : R) := by
      by_contra g
      rw [← mem_nonunits_iff] at g
      rw [← IsLocalRing.mem_maximalIdeal] at g
      have a_cast_zero := Ideal.Quotient.eq_zero_iff_mem.2 g
      rw [map_natCast] at a_cast_zero
      have r_dvd_a := (ringChar.spec K a).1 a_cast_zero
      exact absurd r_dvd_a r_ne_dvd_a
    have rn_cast_zero : ↑(r ^ n) = (0 : R) := by
      rw [← one_mul (↑(r ^ n) : R), ← a_unit.val_inv_mul, mul_assoc, ← Nat.cast_mul,
        ← q_eq_a_mul_rn, CharP.cast_eq_zero R q, mul_zero]
    have q_eq_rn := Nat.dvd_antisymm ((CharP.cast_eq_zero_iff R q (r ^ n)).mp rn_cast_zero) rn_dvd_q
    have n_pos : n ≠ 0 := fun n_zero =>
      absurd (by simpa [n_zero] using q_eq_rn) (CharP.char_ne_one R q)
    -- Definition of prime power: `∃ r n, Prime r ∧ 0 < n ∧ r ^ n = q`.
    exact ⟨r, ⟨n, ⟨r_prime.prime, ⟨pos_iff_ne_zero.mpr n_pos, q_eq_rn.symm⟩⟩⟩⟩
  · have K_char_p_0 := ringChar.of_eq r_zero
    have K_char_zero : CharZero K := CharP.charP_to_charZero K
    have R_char_zero := RingHom.charZero (IsLocalRing.residue R)
    -- Finally, `r = 0` would lead to a contradiction:
    have q_zero := CharP.eq R char_R_q (CharP.ofCharZero R)
    exact absurd q_zero q_pos

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

Goal state before:
pp: case inr.inr
α : 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₁ s₂ : Seq α
ih : motive s₁ s₂
hd : α
s₁' s₂' : Seq α
h✝ : s₁ = cons hd s₁' ∧ s₂ = cons hd s₂' ∧ motive s₁' s₂'
⊢ s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

Tactic:
· grind

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

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.append nil = s

Tactic:
apply coinduction2 s

Goal state after:
α : Type u
s : Seq α
⊢ ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = s.append nil ∧ s2 = s) (s.append nil).destruct s.destruct
Module: Mathlib.Data.Seq.Computation

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

Tactic:
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'
⊢ BisimO (fun c₁ c₂ ↦ (c₂ <|> (empty α).think) = c₁) (s.think <|> (empty α).think).destruct s.think.destruct

Tactic:
simp only [BisimO, orElse_think, destruct_think]; rw [← think_empty]

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
v : K
h : Int.fract v ≠ 0
H : (IntFractPair.of v).fr = Int.fract v
⊢ some (IntFractPair.of (IntFractPair.of v).fr⁻¹) = some (IntFractPair.of (Int.fract v)⁻¹)

Tactic:
H

Goal state after:
case zero
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
H : (IntFractPair.of v).fr = Int.fract v
⊢ some (IntFractPair.of (Int.fract v)⁻¹) = some (IntFractPair.of (Int.fract v)⁻¹)
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: case ih
ι : 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
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), (g✝ i) a = 0 → a = 0
i✝ : ι
g : G i✝
hz : (lift G f P g✝ Hg) ((of G f i✝) g) = 0
⊢ (of G f i✝) g = 0

Tactic:
rw [lift_of] at hz

Goal state after:
case ih
ι : 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
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), (g✝ i) a = 0 → a = 0
i✝ : ι
g : G i✝
hz : (g✝ i✝) g = 0
⊢ (of G f i✝) g = 0
Module: Mathlib.Data.Seq.Basic

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

Tactic:
by
  convert! zipWith_map _ _ (@id α) _ _
  simp

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

Goal state before:
pp: case pos.cons
α : 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
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
b_hd : β
b_tl : Seq β
this : motive (a.drop (a.length ha)) (cons b_hd b_tl)
hb_cons : cons b_hd b_tl ≠ nil
a_hd : α
a_tl : Seq α
right✝ : motive a_tl b_tl
ha' : 0 = a_tl.length' + 1
⊢ False

Tactic:
generalize a_tl.length' = u at ha'

Goal state after:
case pos.cons
α : 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
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
b_hd : β
b_tl : Seq β
this : motive (a.drop (a.length ha)) (cons b_hd b_tl)
hb_cons : cons b_hd b_tl ≠ nil
a_hd : α
a_tl : Seq α
right✝ : motive a_tl b_tl
u : ℕ∞
ha' : 0 = u + 1
⊢ False
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
⊢ (Seq.map ret s).join = s

Tactic:
apply coinduction2 s

Goal state after:
α : Type u
s : Seq α
⊢ ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret s).join.destruct s.destruct
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim.nil.cons
α : Type u
SS✝ : Seq (Seq1 (Seq1 α))
S : Seq1 (Seq1 α)
SS : Seq (Seq1 (Seq1 α))
⊢ BisimO (fun s1 s2 ↦ ∃ s SS, s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join)
    (nil.append (Seq.cons S SS).join.join).destruct (nil.append (Seq.map join (Seq.cons S SS)).join).destruct

Tactic:
obtain ⟨⟨x, s⟩, S⟩ := S

Goal state after:
case bisim.nil.cons
α : Type u
SS✝ SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x : α
s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s SS, s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join)
    (nil.append (Seq.cons ((x, s), S) SS).join.join).destruct
    (nil.append (Seq.map join (Seq.cons ((x, s), S) SS)).join).destruct
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
not_terminatedAt_n : ¬g.TerminatedAt n
this : g.convs (n + 1) = g'.convs n
⊢ g.convs (n + 1) = g'.convs' n

Tactic:
by
        -- invoke the IH for the squashed gcf
        rwa [← IH]
        intro gp' m m_lt_n s_mth_eq'
        -- case distinction on m + 1 = n or m + 1 < n
        rcases m_lt_n with n | succ_m_lt_n
        · -- the difficult case at the squashed position: we first obtain the values from
          -- the sequence
          obtain ⟨gp_succ_m, s_succ_mth_eq⟩ : ∃ gp_succ_m, g.s.get? (m + 1) = some gp_succ_m :=
            Option.ne_none_iff_exists'.mp not_terminatedAt_n
          obtain ⟨gp_m, mth_s_eq⟩ : ∃ gp_m, g.s.get? m = some gp_m :=
            g.s.ge_stable m.le_succ s_succ_mth_eq
          -- we then plug them into the recurrence
          suffices 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b by
            have ot : g'.s.get? m = some ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ :=
              squashSeq_nth_of_not_terminated mth_s_eq s_succ_mth_eq
            grind
          have m_lt_n : m < m.succ := Nat.lt_succ_self m
          refine ⟨(s_pos (Nat.lt_succ_of_lt m_lt_n) mth_s_eq).left, ?_⟩
          refine add_pos (s_pos (Nat.lt_succ_of_lt m_lt_n) mth_s_eq).right ?_
          have : 0 < gp_succ_m.a ∧ 0 < gp_succ_m.b := s_pos (lt_add_one <| m + 1) s_succ_mth_eq
          exact div_pos this.left this.right
        · -- the easy case: before the squashed position, nothing changes
          refine s_pos (Nat.lt_succ_of_lt <| Nat.lt_succ_of_lt succ_m_lt_n) ?_
          exact Eq.trans (squashGCF_nth_of_lt succ_m_lt_n).symm s_mth_eq'

Goal state after:
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
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
⊢ 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:
have g_finite_correctness :
      v = GenContFract.compExactValue pred_conts conts ifp.fr :=
    compExactValue_correctness_of_stream_eq_some stream_nth_eq

Goal state after:
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
⊢ 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))
Module: Mathlib.RingTheory.TensorProduct.Free

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
a : A
x✝ x y : A ⊗[R] M
hx : (basisAux A b) (a • x) = a • (basisAux A b) x
hy : (basisAux A b) (a • y) = a • (basisAux A b) y
⊢ (basisAux A b) (a • (x + y)) = a • (basisAux A b) (x + y)

Tactic:
by simp [hx, hy]

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

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
κ : ι → Type u_4
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal fun i ↦ N ↑i
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i)
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ ↑i
hi : σ ↑i ∈ s
⊢ ((h.collectedBasis b).repr (f ↑((b i) k))) ⟨i, k⟩ = 0

Tactic:
let j : s := ⟨σ i, hi⟩
    replace hσ : j ≠ i := fun hij ↦ hσ i <| Subtype.ext_iff.mp hij
    exact h.collectedBasis_repr_of_mem_ne b hσ <| hf _ <| Subtype.mem (b i k)

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
⊢ (ρ • LinearMap.id + f).HasEigenvalue μ ↔ f.HasEigenvalue (μ - ρ)

Tactic:
have aux : ρ • .id + f - μ • 1 = f - (μ - ρ) • 1 := by module
  simp only [hasEigenvalue_iff, eigenspace_def, aux]

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

Goal state before:
pp: case pos
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2
⊢ Red (hd1 :: tl1) tl2

pp: case neg
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : ¬(hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2)
⊢ Red (hd1 :: tl1) (hd1 :: hd2 :: tl2)

Tactic:
· cases hd1
        cases hd2
        cases h
        dsimp at *
        subst_vars
        apply Red.trans (Red.cons_cons ih)
        exact Red.Step.cons_not_rev.to_red

Goal state after:
case neg
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : ¬(hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2)
⊢ Red (hd1 :: tl1) (hd1 :: hd2 :: tl2)
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : x = y ∧ b = !c
H : tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ p

Tactic:
H

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: (L2 ++ (x', b') :: (x', !b') :: L3)
h : x = y ∧ b = !c
H : tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ p
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case neg.cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
head_eq✝ : (x, b) = a
H : (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3

Tactic:
H

Goal state after:
case neg.cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
head_eq✝ : (x, b) = a
H : (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ L2 ++ (x', b') :: (x', !b') :: L3 = L2 ++ (x', b') :: (x', !b') :: L3
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case mk
α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
⊢ (Quot.mk Red.Step L)⁻¹.toWord = invRev (toWord (Quot.mk Red.Step L))

Tactic:
quot_mk_eq_mk,

Goal state after:
case mk
α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
⊢ (mk L)⁻¹.toWord = invRev (mk L).toWord
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ (of a ^ n).toWord.length = n

Tactic:
toWord_of_pow,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ (List.replicate n (a, true)).length = n
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

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

Tactic:
induction xs with grind [ofList_nil, ofList_cons]

Goal state after:
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:
H

Goal state after:
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
⊢ x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k = x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k
Module: Mathlib.Algebra.Group.Action.Equidecomp

Goal state before:
pp: X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a✝ : X
aA : a✝ ∈ A
aB : a✝ ∈ f ⁻¹' B
⊢ ∃ g_1 ∈ T * S, (g ∘ f) a✝ = g_1 • a✝

Tactic:
rcases hf _ aA with ⟨γ, γ_mem, hγ⟩

Goal state after:
X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a✝ : X
aA : a✝ ∈ A
aB : a✝ ∈ f ⁻¹' B
γ : G
γ_mem : γ ∈ S
hγ : f a✝ = γ • a✝
⊢ ∃ g_1 ∈ T * S, (g ∘ f) a✝ = g_1 • a✝
Module: Mathlib.Algebra.Group.Action.Sigma

Goal state before:
pp: ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → SMul M (α i)
inst✝¹ : (i : ι) → SMul N (α i)
a✝ : M
i : ι
b✝ : α i
x✝ : (i : ι) × α i
inst✝ : ∀ (i : ι), SMulCommClass M N (α i)
a : M
b : N
x : (i : ι) × α i
⊢ a • b • x = b • a • x

Tactic:
by
    cases x
    rw [smul_mk, smul_mk, smul_mk, smul_mk, smul_comm]

Goal state after: