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

Goal state before:
pp: R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
hfBC : Function.Surjective ⇑(ConcreteCategory.hom fBC)
F : (A ⟶ R) × (↑B ⊕ ↑C → ↑R) → ((A ⟶ R) × (↑B → ↑R)) × (A ⟶ R) × (↑C → ↑R) :=
  fun x ↦ ((x.1, x.2 ∘ Sum.inl), x.1, x.2 ∘ Sum.inr)
hF : IsEmbedding F
H : IsEmbedding (Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm)
⊢ IsEmbedding ((Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x) ∘ fun f ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f))

Tactic:
convert!
    ((H.comp hF).comp (mvPolynomialHomeomorph _ R A).isEmbedding).comp
      (isEmbedding_precomp_of_surjective (R := R) fBC hfBC)

Goal state after:
R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
hfBC : Function.Surjective ⇑(ConcreteCategory.hom fBC)
F : (A ⟶ R) × (↑B ⊕ ↑C → ↑R) → ((A ⟶ R) × (↑B → ↑R)) × (A ⟶ R) × (↑C → ↑R) :=
  fun x ↦ ((x.1, x.2 ∘ Sum.inl), x.1, x.2 ∘ Sum.inr)
hF : IsEmbedding F
H : IsEmbedding (Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm)
⊢ ((Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x) ∘ fun f ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f)) =
    ((Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm ∘ F) ∘
        ⇑(mvPolynomialHomeomorph (↑B ⊕ ↑C) R A)) ∘
      fun x ↦ fBC ≫ x
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: 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
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₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
d : M₁
hz₁ : z₁ - z₂ = i₁ d
hd : f₁ d = y₁ - y₂
⊢ π₁ (i₁ d) = 0

Tactic:
hπ₁

Goal state after:
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
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₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
d : M₁
hz₁ : z₁ - z₂ = i₁ d
hd : f₁ d = y₁ - y₂
⊢ i₁ d ∈ Set.range ⇑i₁
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 : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s :
  PushoutCocone ((pair (Under.mk f) (Under.mk g)).obj { as := WalkingPair.left }).hom
    ((pair (Under.mk f) (Under.mk g)).obj { as := WalkingPair.right }).hom
m : (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).right ⟶ s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ m = Under.Hom.right (hc.desc (pushoutCoconeEquivBinaryCofan.functor.obj s))

Tactic:
by
      change PushoutCocone f g at s
      have := hc.uniq (pushoutCoconeEquivBinaryCofan.functor.obj s) (Under.homMk m <| by
        simp [← hm₁, dsimp% c.inl.w_assoc])
        (by rintro (_ | _) <;> ext <;> simpa)
      exact congr(($this).right)

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
X Y Z : T
inst✝ : P.IsStableUnderComposition
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
⊢ map Q ⋯ = map Q hg ⋙ map Q hf

Tactic:
fapply Functor.ext
  · simp [map, Comma.mapLeft, CategoryTheory.Comma.mapLeft, Comma.lift]
  · intro U V k
    ext
    simp

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_zero : r = 0
K_char_p_0 : CharP K 0
K_char_zero : CharZero K
R_char_zero : CharZero R
⊢ IsPrimePow q

Tactic:
have q_zero := CharP.eq R char_R_q (CharP.ofCharZero R)

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_zero : r = 0
K_char_p_0 : CharP K 0
K_char_zero : CharZero K
R_char_zero : CharZero R
q_zero : q = 0
⊢ IsPrimePow q
Module: Mathlib.Algebra.CharP.MixedCharZero

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

Tactic:
by_cases h : ∃ p > 0, MixedCharZero R p
  · rcases h with ⟨p, ⟨H, hp⟩⟩
    rw [← MixedCharZero.reduce_to_p_prime] at h_mixed
    exact h_mixed p H hp
  · apply h_equal
    rw [← isEmpty_algebraRat_iff_mixedCharZero, not_isEmpty_iff] at h
    exact h.some

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

Goal state before:
pp: case mpr
α : Type u
x x' : α
s s' : Seq α
left✝ : x = x'
right✝ : s = s'
⊢ cons x s = cons x' s'

Tactic:
congr

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : α → α
a : α
⊢ map f (iterate g a) = f a :: corec f g (g a)

Tactic:
map_eq,

Goal state after:
α : Type u
β : Type v
f : α → β
g : α → α
a : α
⊢ f (iterate g a).head :: map f (iterate g a).tail = f a :: corec f g (g a)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
s₁ s₂ : Stream' α
x✝ : a ∈ s₂
n : ℕ
h : (fun b ↦ a = b) (s₂.get n)
⊢ (fun b ↦ a = b) ((s₁ ⋈ s₂).get (2 * n + 1))

Tactic:
rw [h, get_interleave_right]

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

Goal state before:
pp: α : Type u
a₁ a₂ : α
s : Stream' α
⊢ (a₁ :: a₂ :: s).even = a₁ :: s.even

Tactic:
unfold even
  rw [corec_eq]; rfl

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

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.TerminatedAt 0 ↔ s = nil

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case refine_1
α : Type u
s : Seq α
⊢ s.TerminatedAt 0 → s = nil

case refine_2
α : Type u
s : Seq α
⊢ s = nil → s.TerminatedAt 0
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
x : α
h : x ∈ s
⊢ ∃ i, some x = s.get? i

Tactic:
change (some x ∈ s.1) at h

Goal state after:
α : Type u
s : Seq α
x : α
h : some x ∈ ↑s
⊢ ∃ i, some x = s.get? i
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
m n : ℕ
h : m ≤ n
⊢ s.val m = some a → s.val n = some a

Tactic:
obtain ⟨f, al⟩ := s
  induction h with
  | refl => exact id
  | step _ IH => exact fun h2 ↦ al (IH h2)

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

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ ((∃ n, s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none) ↔ s.get? n = none

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case refine_1
α : Type u
s : Seq α
n : ℕ
⊢ ((∃ n, s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none) → s.get? n = none

case refine_2
α : Type u
s : Seq α
n : ℕ
⊢ s.get? n = none → (∃ n, s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none
Module: Mathlib.Data.Seq.Basic

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

Tactic:
refine ⟨?_, ?_⟩

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

case refine_2
α : Type u
s : Seq α
n : ℕ
⊢ ¬s.get? n = none → ∀ (x : ℕ), s.get? x = none → ∀ m ≤ n, ¬s.get? m = none
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g
s : Computation α
⊢ BisimO (fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g)
    ((s.bind f).bind g).destruct (s.bind fun x ↦ (f x).bind g).destruct

Tactic:
induction s using recOn with
      | pure s =>
        simp only [BisimO, ret_bind]; generalize f s = fs
        induction fs using recOn with
        | pure t => rw [ret_bind]; rcases destruct (g t) with b | cb <;> simp
        | think => simp
      | think s => simpa [BisimO] using Or.inr ⟨s, rfl, rfl⟩

Goal state after:
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
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
n : ℕ
z : DirectLimit G fun i j h ↦ ⇑(f' i j h)
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = C z * X ^ n
i : ι
x : G i
h : (of G (fun i j h ↦ ⇑(f' i j h)) i) x = z
⊢ Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) (C x * X ^ (n + 1)) = C z * X ^ (n + 1)

Tactic:
Polynomial.map_mul,

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
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
n : ℕ
z : DirectLimit G fun i j h ↦ ⇑(f' i j h)
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = C z * X ^ n
i : ι
x : G i
h : (of G (fun i j h ↦ ⇑(f' i j h)) i) x = z
⊢ Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) (C x) *
      Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) (X ^ (n + 1)) =
    C z * X ^ (n + 1)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
⊢ Nat.find h = s.length ⋯

Tactic:
congr

Goal state after:
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
⊢ (map f s).TerminatedAt = s.TerminatedAt
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case succ.inl
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = none
hnone : IntFractPair.stream (Int.fract v)⁻¹ n = none
⊢ IntFractPair.stream v (n + 1 + 1) = none

Tactic:
succ_nth_stream_eq_none_iff.mpr (Or.inl ih)

Goal state after:
case succ.inl
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = none
hnone : IntFractPair.stream (Int.fract v)⁻¹ n = none
⊢ none = none
Module: Mathlib.Data.Seq.Basic

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

Tactic:
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.Seq.Basic

Goal state before:
pp: case succ
α : Type u
s : Seq α
x : α
n✝ : ℕ
⊢ Option.map (Prod.mk (n✝ + 1)) (s.get? n✝) = Option.map (Prod.map Nat.succ id ∘ Prod.mk n✝) (s.get? n✝)

Tactic:
congr

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

Goal state before:
pp: α : Type u
β : Type v
init : β
f : β → α → β
x : α
s : Seq α
⊢ cons init
      (corec
        (fun x ↦
          match x.2.destruct with
          | none => none
          | some (x_1, s) => some (f x.1 x_1, f x.1 x_1, s))
        (init, cons x s)) =
    cons init
      (cons (f init x)
        (corec
          (fun x ↦
            match x.2.destruct with
            | none => none
            | some (x_1, s) => some (f x.1 x_1, f x.1 x_1, s))
          (f init x, s)))

Tactic:
congr

Goal state after:
case e_s
α : Type u
β : Type v
init : β
f : β → α → β
x : α
s : Seq α
⊢ corec
      (fun x ↦
        match x.2.destruct with
        | none => none
        | some (x_1, s) => some (f x.1 x_1, f x.1 x_1, s))
      (init, cons x s) =
    cons (f init x)
      (corec
        (fun x ↦
          match x.2.destruct with
          | none => none
          | some (x_1, s) => some (f x.1 x_1, f x.1 x_1, s))
        (f init x, s))
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n ≠ none
p : Pair K
hp : (of (fract v)⁻¹).s.get? n = some p
p' : IntFractPair K
hp'₁ : IntFractPair.stream v (n + 1 + 1) = some p'
right✝ : ↑p'.b = p.b
Hp : (of (fract v)⁻¹).s.get? n = some { a := 1, b := ↑p'.b }
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n

Tactic:
rw [Hp, get?_of_eq_some_of_succ_get?_intFractPair_stream hp'₁]

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

Goal state before:
pp: α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ (Seq.cons hd tl).get? i
⊢ ∀ y ∈ (Seq.cons hd tl).get? j, R x y

Tactic:
y

Goal state after:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ (Seq.cons hd tl).get? i
y : α
⊢ y ∈ (Seq.cons hd tl).get? j → R x y
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ s.get? i
⊢ ∀ y ∈ s.get? j, R x y

Tactic:
y

Goal state after:
α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ s.get? i
y : α
⊢ y ∈ s.get? j → R x y
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
R : α → α → Prop
inst✝ : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
h_succ : ∀ {n : ℕ} {x y : α}, s.get? n = some x → s.get? (n + 1) = some y → R x y
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ s.get? i
⊢ ∀ y ∈ s.get? j, R x y

Tactic:
y

Goal state after:
α : Type u
R : α → α → Prop
inst✝ : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
h_succ : ∀ {n : ℕ} {x y : α}, s.get? n = some x → s.get? (n + 1) = some y → R x y
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ s.get? i
y : α
⊢ y ∈ s.get? j → R x y
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
gp_n : Pair K
nth_s_eq : (of v).s.get? n = some gp_n
nth_partDen_eq : (of v).partDens.get? n = some gp_n.b
⊢ 1 ≤ gp_n.b

Tactic:
obtain ⟨ifp_n, succ_nth_stream_eq, ifp_n_b_eq_gp_n_b⟩ :
      ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ (ifp.b : K) = gp_n.b :=
    IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some nth_s_eq

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
gp_n : Pair K
nth_s_eq : (of v).s.get? n = some gp_n
nth_partDen_eq : (of v).partDens.get? n = some gp_n.b
ifp_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_n
ifp_n_b_eq_gp_n_b : ↑ifp_n.b = gp_n.b
⊢ 1 ≤ gp_n.b
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
x y z : S
⊢ 1 * (X - C x) * (X - C y) * (X - C z) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly

Tactic:
← C_1,

Goal state after:
S : Type u_2
inst✝ : CommRing S
x y z : S
⊢ C 1 * (X - C x) * (X - C y) * (X - C z) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P Q : Cubic R
inst✝ : Semiring R
h : P.toPoly = Q.toPoly
⊢ P.a = Q.a

Tactic:
← coeff_eq_a,

Goal state after:
R : Type u_1
P Q : Cubic R
inst✝ : Semiring R
h : P.toPoly = Q.toPoly
⊢ P.toPoly.coeff 3 = Q.a
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
x : R
i : I
⊢ ↑(((decompose V) x) i) = ↑(x • ((decompose V) 1) i)

Tactic:
← smul_apply,

Goal state after:
R : Type u_1
I : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq I
V : I → Ideal R
inst✝ : Decomposition V
x : R
i : I
⊢ ↑(((decompose V) x) i) = ↑((x • (decompose V) 1) i)
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case pos
R : Type u_1
P : Cubic R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : P.toPoly = 0
⊢ P.toPoly.roots.card ≤ 3

Tactic:
simp [hP]

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
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
⊢ |v - g.convs n| ≤ 1 / (conts.b * nextConts.b)

Tactic:
have gp_a_eq_one : gp.a = 1 := of_partNum_eq_one (partNum_eq_s_a s_nth_eq)

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
⊢ |v - g.convs n| ≤ 1 / (conts.b * nextConts.b)
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
i : ι
⊢ (basis A b).repr.symm (Finsupp.single i a) = a ⊗ₜ[R] b.repr.symm (Finsupp.single i 1)

Tactic:
simp [basis, Equiv.uniqueProd_symm_apply, basisAux]

Goal state after:
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv

Goal state before:
pp: K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →ₗ[K] W := applyₗ z ∘ₗ f.toLinearMap ∘ₗ smulRightₗ v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
A : End K V
x : V
⊢ (f (smulRight v (A x))) z = (f (A * smulRight v x)) z

Tactic:
congr

Goal state after:
case e_6
K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →ₗ[K] W := ⋯
hT : ∀ (x : V), T x = (f (smulRight v x)) z
A : End K V
x : V
⊢ smulRight v (A x) = A * smulRight v x
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv

Goal state before:
pp: case neg
K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →ₗ[K] W := applyₗ z ∘ₗ f.toLinearMap ∘ₗ smulRightₗ v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
this : ∀ (A : End K V) (x : V), T (A x) = (f A) (T x)
⊢ ∃ T, ∀ (a : End K V), f a ∘ₗ ↑T = ↑T ∘ₗ a

Tactic:
have surj : Function.Surjective T := fun w ↦ by
    obtain ⟨d, hd⟩ := Projective.exists_dual_eq_one K hz
    exact ⟨f.symm (smulRight d w) u, by simp [T, this, hd]⟩

Goal state after:
case neg
K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →ₗ[K] W := applyₗ z ∘ₗ f.toLinearMap ∘ₗ smulRightₗ v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
this : ∀ (A : End K V) (x : V), T (A x) = (f A) (T x)
surj : Function.Surjective ⇑T
⊢ ∃ T, ∀ (a : End K V), f a ∘ₗ ↑T = ↑T ∘ₗ a
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
μ : R
hf : f.HasUnifEigenvalue μ 1
m : M
hm : f.HasUnifEigenvector μ 1 m
n : ℕ
hn : f ^ n = 0
⊢ μ ^ n = 0

Tactic:
simpa [hn, hm.2, eq_comm (a := (0 : M))] using hm.pow_apply n

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

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
i j : n
x y : R
⊢ c.ofMatrix x y → Relation.Map (⇑c) (fun x ↦ x i j) (fun x ↦ x i j) x y

pp: case mpr
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
i j : n
x y : R
⊢ Relation.Map (⇑c) (fun x ↦ x i j) (fun x ↦ x i j) x y → c.ofMatrix x y

Tactic:
· intro h
    refine ⟨_,_, h i j, ?_⟩
    simp

Goal state after:
case mpr
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
i j : n
x y : R
⊢ Relation.Map (⇑c) (fun x ↦ x i j) (fun x ↦ x i j) x y → c.ofMatrix x y