mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝ : F
⊢ 0 * x✝ = 0

Tactic:
by apply DFunLike.ext; simp

Goal state after:
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
f : F
⊢ f * 0 = 0

Tactic:
by apply DFunLike.ext; simp

Goal state after:
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
f g h : F
⊢ f * (g + h) = f * g + f * h

Tactic:
by apply DFunLike.ext; simp

Goal state after:
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
x✝² x✝¹ x✝ : F
⊢ (x✝² + x✝¹) * x✝ = x✝² * x✝ + x✝¹ * x✝

Tactic:
by apply DFunLike.ext; simp

Goal state after:
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
⊢ ↑0 = 0

Tactic:
by apply DFunLike.ext; simp

Goal state after:
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝²² : FunLike F α α
inst✝²¹ : Zero F
inst✝²⁰ : One F
inst✝¹⁹ : Mul F
inst✝¹⁸ : Add F
inst✝¹⁷ : Neg F
inst✝¹⁶ : Sub F
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : IsZeroApply F α α
inst✝¹³ : IsAddApply F α α
inst✝¹² : IsOneApplyEqSelf F α
inst✝¹¹ : IsMulApplyEqComp F α
inst✝¹⁰ : IsNegApply F α α
inst✝⁹ : IsSubApply F α α
inst✝⁸ : SMul ℕ F
inst✝⁷ : IsSMulApply ℕ F α α
inst✝⁶ : SMul ℤ F
inst✝⁵ : IsSMulApply ℤ F α α
inst✝⁴ : AddMonoidHomClass F α α
inst✝³ : NatCast F
inst✝² : IsNatCastApply F α
inst✝¹ : IntCast F
inst✝ : IsIntCastApply F α
x✝ : ℕ
⊢ IntCast.intCast ↑x✝ = ↑x✝

Tactic:
by apply DFunLike.ext; simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ↑↑e
g' : B' →ₛₗ[σ'] A := ↑↑e.symm
h : A →+ B' := ↑e
h' : B' →+ A := ↑e.symm
⊢ sInf (TopologicalSpace.induced ⇑e.toHomeomorph.symm '' {t | ContinuousSMul R A ∧ ContinuousAdd A}) =
    sInf {t | ContinuousSMul S B' ∧ ContinuousAdd B'}

Tactic:
apply congr_arg

Goal state after:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ⋯
g' : B' →ₛₗ[σ'] A := ⋯
h : A →+ B' := ⋯
h' : B' →+ A := ⋯
⊢ TopologicalSpace.induced ⇑e.toHomeomorph.symm '' {t | ContinuousSMul R A ∧ ContinuousAdd A} =
    {t | ContinuousSMul S B' ∧ ContinuousAdd B'}
Module: Mathlib.CategoryTheory.Preadditive.Injective.Preserves

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : EnoughInjectives D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesInjectiveObjects
X Y : C
f : X ⟶ Y
x✝ : Mono f
⊢ ∃ h, F.map f ≫ h = Injective.ι (F.obj X)

Tactic:
exact ⟨F.map (Injective.factorThru (adj.unit.app X ≫ G.map (Injective.ι _)) f) ≫
      adj.counit.app (Injective.under (F.obj X)), by simp [← Functor.map_comp_assoc]⟩

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Ring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
x✝¹ : T
x✝ : S
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (↑(LinearEquiv.restrictScalars R (TensorProduct.AlgebraTensorModule.distribBaseChange R T S S)) ∘ₗ
            LinearMap.lTensor T (includeLeftSubRight R S)))
        x✝¹)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (↑R (includeLeftSubRight T (T ⊗[R] S)))) x✝¹) x✝

Tactic:
simp [TensorProduct.tmul_sub, TensorProduct.one_def, tmul_one_tmul_one_tmul]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X✝ : I → TopModuleCat R
f✝ : (i : I) → (X✝ i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
X Y : J
f : X ⟶ Y
⊢ F.map f ≫ toCoinduced c.ι.app Y = toCoinduced c.ι.app X ≫ ((Functor.const J).obj (coinduced c.ι.app)).map f

Tactic:
ext x; exact congr($(c.ι.naturality f).hom x)

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
e : F✝ ≅ G✝
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsCardinalAccessible κ
inst✝ : G.IsCardinalAccessible κ
⊢ (F ⋙ G).IsCardinalAccessible κ

Tactic:
(Term.byTactic
 "by"
 (Tactic.tacticSeq
  (Tactic.tacticSeq1Indented
   [(Tactic.tacticHave__
     "have"
     (Term.letConfig [])
     (Term.letDecl
      (Term.letIdDecl
       (Term.letId (hygieneInfo `[anonymous]))
       []
       []
       ":="
       (Term.app `F.preservesColimitsOfShape_of_isCardinalAccessible [`κ]))))
    []
    (Tactic.tacticHave__
     "have"
     (Term.letConfig [])
     (Term.letDecl
      (Term.letIdDecl
       (Term.letId (hygieneInfo `[anonymous]))
       []
       []
       ":="
       (Term.app `G.preservesColimitsOfShape_of_isCardinalAccessible [`κ]))))
    []
    (Tactic.exact
     "exact"
     (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))])))

Goal state after:
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
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₃
H : (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0
y : M₁
hy : i₁ y = ρ (i₂ (σ (ι₃ x)))
⊢ g₁ (i₁ y) - i₂ (f₁ y) = 0

Tactic:
sub_eq_zero

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
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₃
H : (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0
y : M₁
hy : i₁ y = ρ (i₂ (σ (ι₃ x)))
⊢ g₁ (i₁ y) = i₂ (f₁ y)
Module: Mathlib.Algebra.CharP.Algebra

Goal state before:
pp: case zero
R : Type u_1
A : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring A
f : R →+* A
h : Function.Injective ⇑f
inst✝ : CharZero R
⊢ ExpChar A 1

pp: case prime
R : Type u_1
A : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring A
f : R →+* A
h : Function.Injective ⇑f
q : ℕ
hprime : Nat.Prime q
hchar✝ : CharP R q
⊢ ExpChar A q

Tactic:
· have := charZero_of_injective_ringHom h; exact .zero

Goal state after:
case prime
R : Type u_1
A : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring A
f : R →+* A
h : Function.Injective ⇑f
q : ℕ
hprime : Nat.Prime q
hchar✝ : CharP R q
⊢ ExpChar A q
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))
⊢ ↑1 = 1

Tactic:
by
  apply Units.ext
  rw [Units.val_one]
  change ((PNat.isUnit_natCast (R := R) 1).unit : R) = 1
  rw [IsUnit.unit_spec (PNat.isUnit_natCast 1)]
  rw [PNat.one_coe, Nat.cast_one]

Goal state after:
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))
n : ℕ+
⊢ ↑↑n = ↑↑n

Tactic:
by
  change ((PNat.isUnit_natCast (R := R) n).unit : R) = ↑n
  simp only [IsUnit.unit_spec]

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

Goal state before:
pp: α : Type u
m n : ℕ
h : m ≤ n
f : Stream' (Option α)
al : f.IsSeq
⊢ get? ⟨f, al⟩ m = none → get? ⟨f, al⟩ n = none

Tactic:
induction h with | refl => exact id | step _ IH => exact fun h2 ↦ al (IH h2)

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 : ℕ
⊢ (y :: t).get n.succ = t.get n

Tactic:
get_succ_cons

Goal state after:
α : Type u
x y : α
s t : Stream' α
h : x :: s = y :: t
n : ℕ
⊢ t.get n = t.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:
rw [← Stream'.eta (map f s), tail_map, head_map]

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

Goal state before:
pp: case none
α : Type u
s s' : Computation α
f0 : s.val 0 = none
h' : s.tail = s'
⊢ s = s'.think

Tactic:
← h'

Goal state after:
case none
α : Type u
s s' : Computation α
f0 : s.val 0 = none
h' : s.tail = s'
⊢ s = s.tail.think
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 := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
ih : s₁ = 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:
rcases ih with (rfl | ih)

Goal state after:
case inl
α : 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₁ = nil ∧ s₁ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

case 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₂
⊢ s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩) = Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b'), ⋯⟩

Tactic:
apply congr_arg

Goal state after:
case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩ = ⟨Stream'.corec' (Corec.f f) (Sum.inr b'), ⋯⟩
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_1.refine_1
α : 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' : Computation α
r' : α
⊢ ∀ (a : α),
    R (pure r') (pure a) →
      BisimO R (pure r').destruct (pure a).destruct → (pure r').head = (pure a).head ∧ R (pure r').tail (pure a).tail

Tactic:
intro a'

Goal state after:
case refine_1.refine_1
α : 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' : Computation α
r' a' : α
⊢ R (pure r') (pure a') →
    BisimO R (pure r').destruct (pure a').destruct → (pure r').head = (pure a').head ∧ R (pure r').tail (pure a').tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_1.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' : Computation α
r' : α
⊢ ∀ (s : Computation α),
    R (pure r') s.think →
      BisimO R (pure r').destruct s.think.destruct → (pure r').head = s.think.head ∧ R (pure r').tail s.think.tail

Tactic:
intro a'

Goal state after:
case refine_1.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' : Computation α
r' : α
a' : Computation α
⊢ R (pure r') a'.think →
    BisimO R (pure r').destruct a'.think.destruct → (pure r').head = a'.think.head ∧ R (pure r').tail a'.think.tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_2.refine_1
α : 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' : Computation α
⊢ ∀ (a : α),
    R r'.think (pure a) →
      BisimO R r'.think.destruct (pure a).destruct → r'.think.head = (pure a).head ∧ R r'.think.tail (pure a).tail

Tactic:
intro a'

Goal state after:
case refine_2.refine_1
α : 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' : Computation α
a' : α
⊢ R r'.think (pure a') →
    BisimO R r'.think.destruct (pure a').destruct → r'.think.head = (pure a').head ∧ R r'.think.tail (pure a').tail
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' : Computation α
⊢ ∀ (s : Computation α),
    R r'.think s.think →
      BisimO R r'.think.destruct s.think.destruct → r'.think.head = s.think.head ∧ R r'.think.tail s.think.tail

Tactic:
intro a'

Goal state after:
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'.think a'.think →
    BisimO R r'.think.destruct a'.think.destruct → r'.think.head = a'.think.head ∧ R r'.think.tail a'.think.tail
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.tails.tail.get n = drop n s.tail.tail

Tactic:
tails_eq,

Goal state after:
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
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s : Stream' α
⊢ s.tails.get n = drop n s.tail

Tactic:
induction n generalizing s with
  | zero => rfl
  | succ n ih => rw [get_succ, drop_succ, tails_eq, tail_cons, ih]

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
h : LiftRel R ca cb
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
⊢ R a b

Tactic:
by
      let ⟨b', mb', ab⟩ := h.left ma
      rwa [mem_unique mb mb']

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
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
x : FreeCommRing ((i : ι) × G i)
hx :
  x ∈
    {a |
      (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
        (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
          (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
            ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}
⊢ x ∈ Ideal.comap (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) ⊥

Tactic:
Ideal.mem_comap,

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
x : FreeCommRing ((i : ι) × G i)
hx :
  x ∈
    {a |
      (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
        (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
          (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
            ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}
⊢ (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) x ∈ ⊥
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
oe : Option.map f (some a) = some b
⊢ ∃ a ∈ ⟨g, al⟩, f a = b

Tactic:
· injection oe with h'; exact ⟨a, om, h'⟩

Goal state after:
Module: Mathlib.Data.Nat.DvdSequence

Goal state before:
pp: n : ℕ
⊢ IsStrongDvdSequence fun x ↦ n

Tactic:
simp [IsStrongDvdSequence]

Goal state after:
Module: Mathlib.Data.Nat.DvdSequence

Goal state before:
pp: n : ℕ
⊢ IsStrongDvdSequence fun x ↦ n

Tactic:
by
  simp [IsStrongDvdSequence]

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

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

Tactic:
add_right_comm

Goal state after:
n : ℕ
⊢ fib (n + 2) < fib (n + 2 + 1)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim.nil.cons.cons
α : Type u
SS✝ SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x✝ 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✝, Seq.cons x s), S) SS).join.join).destruct
    (nil.append (Seq.map join (Seq.cons ((x✝, Seq.cons x s), S) SS)).join).destruct

Tactic:
simpa using ⟨Seq.cons x (append s (Seq.join S)), SS, by simp, by simp⟩

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

Goal state before:
pp: case bisim.nil
α : Type u
SS✝ 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 SS.join.join).destruct (nil.append (Seq.map join SS).join).destruct

Tactic:
cases SS with
      | nil => simp
      | cons S SS =>
        obtain ⟨⟨x, s⟩, S⟩ := S
        cases s with
        | nil => simpa using ⟨_, _, rfl, rfl⟩
        | cons x s => simpa using ⟨Seq.cons x (append s (Seq.join S)), SS, by simp, by simp⟩

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

Goal state before:
pp: case succ.some.inr
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)

Tactic:
have : (fr : K)⁻¹ = ((fr⁻¹ : ℚ) : K) := by norm_cast
        have coe_of_fr := coe_of_rat_eq this
        simpa [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_ne_zero]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
G : ι → Type u_3
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (G i)
inst✝ : CommMonoid R
ψ χ : (i : ι) → AddChar (G i) R
h : (fun ψ i ↦ toAddMonoidHomEquiv (ψ i)) ψ = (fun ψ i ↦ toAddMonoidHomEquiv (ψ i)) χ
⊢ ψ = χ

Tactic:
simpa [funext_iff] using h

Goal state after: