harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.π_comp_eqToHom (f : J → C) [HasBiproduct f] {j j' : J} (w : j = j') :
    biproduct.π f j ≫ eqToHom (by simp [w]) = biproduct.π f j'

Proof state:
case refl
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j : J
⊢ π f j ≫ eqToHom ⋯ = π f j

Tactic:
simp

Result:
no goals

Proof state:
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j j' : J
w : j = j'
⊢ π f j ≫ eqToHom ⋯ = π f j'

Tactic:
cases w

Result:
case refl
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j : J
⊢ π f j ≫ eqToHom ⋯ = π f j

Proof state:
J✝ : Type w
C✝ : Type uC
inst✝⁶ : Category.{uC', uC} C✝
inst✝⁵ : HasZeroMorphisms C✝
D : Type uD
inst✝⁴ : Category.{uD', uD} D
inst✝³ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j j' : J
w : j = j'
⊢ f j = f j'

Tactic:
simp [w]

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
lemma hom_ext_succ {F G : ComposableArrows C (n + 1)} {f g : F ⟶ G}
    (h₀ : app' f 0 = app' g 0) (h₁ : δ₀Functor.map f = δ₀Functor.map g) : f = g

Proof state:
case w.h.mk.succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : δ₀Functor.map f = δ₀Functor.map g
i : ℕ
hi : i + 1 < n + 1 + 1
⊢ f.app ⟨i + 1, hi⟩ = g.app ⟨i + 1, hi⟩

Tactic:
exact congr_app h₁ ⟨i, by valid⟩

Result:
no goals

Proof state:
case w.h.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : δ₀Functor.map f = δ₀Functor.map g
i : ℕ
hi : i < n + 1 + 1
⊢ f.app ⟨i, hi⟩ = g.app ⟨i, hi⟩

Tactic:
obtain _ | i := i

Result:
case w.h.mk.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : δ₀Functor.map f = δ₀Functor.map g
hi : 0 < n + 1 + 1
⊢ f.app ⟨0, hi⟩ = g.app ⟨0, hi⟩

case w.h.mk.succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : δ₀Functor.map f = δ₀Functor.map g
i : ℕ
hi : i + 1 < n + 1 + 1
⊢ f.app ⟨i + 1, hi⟩ = g.app ⟨i + 1, hi⟩

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : δ₀Functor.map f = δ₀Functor.map g
⊢ f = g

Tactic:
ext ⟨i, hi⟩

Result:
case w.h.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : δ₀Functor.map f = δ₀Functor.map g
i : ℕ
hi : i < n + 1 + 1
⊢ f.app ⟨i, hi⟩ = g.app ⟨i, hi⟩

Proof state:
case w.h.mk.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : δ₀Functor.map f = δ₀Functor.map g
hi : 0 < n + 1 + 1
⊢ f.app ⟨0, hi⟩ = g.app ⟨0, hi⟩

Tactic:
exact h₀

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : δ₀Functor.map f = δ₀Functor.map g
i : ℕ
hi : i + 1 < n + 1 + 1
⊢ i < n + 1

Tactic:
valid

Result:
no goals
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem truncate_comp {n₁ n₂ n₃ : ℕ} (h1 : n₁ ≤ n₂) (h2 : n₂ ≤ n₃) :
    (truncate (p := p) (R := R) h1).comp (truncate h2) = truncate (h1.trans h2)

Proof state:
case a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n₁ n₂ n₃ : ℕ
h1 : n₁ ≤ n₂
h2 : n₂ ≤ n₃
x : TruncatedWittVector p n₃ R
⊢ ((truncate h1).comp (truncate h2)) x = (truncate ⋯) x

Tactic:
simp only [truncate_truncate, Function.comp_apply, RingHom.coe_comp]

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n₁ n₂ n₃ : ℕ
h1 : n₁ ≤ n₂
h2 : n₂ ≤ n₃
⊢ (truncate h1).comp (truncate h2) = truncate ⋯

Tactic:
ext1 x

Result:
case a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n₁ n₂ n₃ : ℕ
h1 : n₁ ≤ n₂
h2 : n₂ ≤ n₃
x : TruncatedWittVector p n₃ R
⊢ ((truncate h1).comp (truncate h2)) x = (truncate ⋯) x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_setIfInBounds_self (v : Vector α n) (i : Nat) (x : α) (hi : i < n) :
    (v.setIfInBounds i x)[i] = x

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
x : α
hi : i < n
⊢ (v.setIfInBounds i x)[i] = x

Tactic:
simp [getElem_setIfInBounds, hi]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem subsingleton (h : 0 ∈ S) : Subsingleton (LocalizedModule S M)

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : 0 ∈ S
⊢ Subsingleton (LocalizedModule S M)

Tactic:
refine ⟨fun a b ↦ ?_⟩

Result:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : 0 ∈ S
a b : LocalizedModule S M
⊢ a = b

Proof state:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : 0 ∈ S
m✝ m'✝ : M
s✝ s'✝ : ↥S
⊢ mk m✝ s✝ = mk m'✝ s'✝

Tactic:
exact mk_eq.mpr ⟨⟨0, h⟩, by simp only [Submonoid.mk_smul, zero_smul]⟩

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : 0 ∈ S
m✝ m'✝ : M
s✝ s'✝ : ↥S
⊢ ⟨0, h⟩ • s'✝ • m✝ = ⟨0, h⟩ • s✝ • m'✝

Tactic:
simp only [Submonoid.mk_smul, zero_smul]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : 0 ∈ S
a b : LocalizedModule S M
⊢ a = b

Tactic:
induction a,b using LocalizedModule.induction_on₂

Result:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : 0 ∈ S
m✝ m'✝ : M
s✝ s'✝ : ↥S
⊢ mk m✝ s✝ = mk m'✝ s'✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_eraseₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {a : α}
    (h : Raw.WFImp m.1) : Raw.WFImp (m.eraseₘ a).1

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
h✝ : m.containsₘ a = true
⊢ Raw.WFImp (m.eraseₘaux a).val

Tactic:
next h' => exact wfImp_eraseₘaux m a h h'

Result:
no goals

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
h✝ : ¬m.containsₘ a = true
⊢ Raw.WFImp m.val

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
h' : m.containsₘ a = true
⊢ Raw.WFImp (m.eraseₘaux a).val

Tactic:
exact wfImp_eraseₘaux m a h h'

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
⊢ Raw.WFImp (if m.containsₘ a = true then m.eraseₘaux a else m).val

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
h✝ : m.containsₘ a = true
⊢ Raw.WFImp (m.eraseₘaux a).val

case isFalse
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
h✝ : ¬m.containsₘ a = true
⊢ Raw.WFImp m.val

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
⊢ Raw.WFImp (m.eraseₘ a).val

Tactic:
rw [eraseₘ]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
⊢ Raw.WFImp (if m.containsₘ a = true then m.eraseₘaux a else m).val
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toList_push (a : Vector α n) (x) : (a.push x).toList = a.toList ++ [x]

Proof state:
α : Type u_1
n : Nat
a : Vector α n
x : α
⊢ (a.push x).toList = a.toList ++ [x]

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Split.lean
theorem hom_ext (f g : X ⟶ Y) (h : ∀ n : ℕ, s.φ f n = s.φ g n) : f = g

Proof state:
case h.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
Δ : SimplexCategoryᵒᵖ
⊢ ∀ (A : IndexSet Δ), (s.cofan Δ).inj A ≫ f.app Δ = (s.cofan Δ).inj A ≫ g.app Δ

Tactic:
intro A

Result:
case h.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ f.app Δ = (s.cofan Δ).inj A ≫ g.app Δ

Proof state:
case h.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ f.app Δ = (s.cofan Δ).inj A ≫ g.app Δ

Tactic:
induction' Δ using Opposite.rec with Δ

Result:
case h.h.op
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
Δ : SimplexCategory
A : IndexSet (op Δ)
⊢ (s.cofan (op Δ)).inj A ≫ f.app (op Δ) = (s.cofan (op Δ)).inj A ≫ g.app (op Δ)

Proof state:
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
Δ : SimplexCategoryᵒᵖ
⊢ f.app Δ = g.app Δ

Tactic:
apply s.hom_ext'

Result:
case h.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
Δ : SimplexCategoryᵒᵖ
⊢ ∀ (A : IndexSet Δ), (s.cofan Δ).inj A ≫ f.app Δ = (s.cofan Δ).inj A ≫ g.app Δ

Proof state:
case h.h.op
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
Δ : SimplexCategory
A : IndexSet (op Δ)
⊢ (s.cofan (op Δ)).inj A ≫ f.app (op Δ) = (s.cofan (op Δ)).inj A ≫ g.app (op Δ)

Tactic:
induction' Δ using SimplexCategory.rec with n

Result:
case h.h.op.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
n : ℕ
A : IndexSet (op ⦋n⦌)
⊢ (s.cofan (op ⦋n⦌)).inj A ≫ f.app (op ⦋n⦌) = (s.cofan (op ⦋n⦌)).inj A ≫ g.app (op ⦋n⦌)

Proof state:
case h.h.op.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
n : ℕ
A : IndexSet (op ⦋n⦌)
⊢ (s.cofan (op ⦋n⦌)).inj A ≫ f.app (op ⦋n⦌) = (s.cofan (op ⦋n⦌)).inj A ≫ g.app (op ⦋n⦌)

Tactic:
simp only [s.cofan_inj_comp_app, h]

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
⊢ f = g

Tactic:
ext Δ

Result:
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
Δ : SimplexCategoryᵒᵖ
⊢ f.app Δ = g.app Δ
-- Mathlib/SetTheory/Cardinal/Finsupp.lean
theorem mk_multiset_of_nonempty (α : Type u) [Nonempty α] : #(Multiset α) = max #α ℵ₀

Proof state:
α : Type u
inst✝ : Nonempty α
⊢ #(Multiset α) = #α ⊔ ℵ₀

Tactic:
classical
exact Multiset.toFinsupp.toEquiv.cardinal_eq.trans (mk_finsupp_nat α)

Result:
no goals

Proof state:
α : Type u
inst✝ : Nonempty α
⊢ #(Multiset α) = #α ⊔ ℵ₀

Tactic:
exact Multiset.toFinsupp.toEquiv.cardinal_eq.trans (mk_finsupp_nat α)

Result:
no goals
-- Mathlib/Tactic/Positivity/Core.lean
lemma nz_of_isRat {n : ℤ} {d : ℕ} [LinearOrderedRing A] :
    (NormNum.IsRat e n d) → (decide (n < 0)) → ((e : A) ≠ 0)
  | ⟨inv, eq⟩, h => by
    have pos_invOf_d : (0 < ⅟ (d : A)) := pos_invOf_of_invertible_cast d
    have neg_n : ((n : A) < 0) := Int.cast_lt_zero (n := n) |>.2 (of_decide_eq_true h)
    have neg := mul_neg_of_neg_of_pos neg_n pos_invOf_d
    rw [eq]
    exact ne_iff_lt_or_gt.2 (Or.inl neg)

Proof state:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n < 0) = true
⊢ e ≠ 0

Tactic:
have pos_invOf_d : (0 < ⅟ (d : A)) := pos_invOf_of_invertible_cast d

Result:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n < 0) = true
pos_invOf_d : 0 < ⅟↑d
⊢ e ≠ 0

Proof state:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n < 0) = true
pos_invOf_d : 0 < ⅟↑d
neg_n : ↑n < 0
⊢ e ≠ 0

Tactic:
have neg := mul_neg_of_neg_of_pos neg_n pos_invOf_d

Result:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n < 0) = true
pos_invOf_d : 0 < ⅟↑d
neg_n : ↑n < 0
neg : ↑n * ⅟↑d < 0
⊢ e ≠ 0

Proof state:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n < 0) = true
pos_invOf_d : 0 < ⅟↑d
⊢ e ≠ 0

Tactic:
have neg_n : ((n : A) < 0) := Int.cast_lt_zero (n := n) |>.2 (of_decide_eq_true h)

Result:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n < 0) = true
pos_invOf_d : 0 < ⅟↑d
neg_n : ↑n < 0
⊢ e ≠ 0

Proof state:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n < 0) = true
pos_invOf_d : 0 < ⅟↑d
neg_n : ↑n < 0
neg : ↑n * ⅟↑d < 0
⊢ e ≠ 0

Tactic:
rw [eq]

Result:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n < 0) = true
pos_invOf_d : 0 < ⅟↑d
neg_n : ↑n < 0
neg : ↑n * ⅟↑d < 0
⊢ ↑n * ⅟↑d ≠ 0

Proof state:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n < 0) = true
pos_invOf_d : 0 < ⅟↑d
neg_n : ↑n < 0
neg : ↑n * ⅟↑d < 0
⊢ ↑n * ⅟↑d ≠ 0

Tactic:
exact ne_iff_lt_or_gt.2 (Or.inl neg)

Result:
no goals
-- Mathlib/Algebra/Ring/Ext.lean
theorem toDistrib_injective : Function.Injective (@toDistrib R)

Proof state:
R : Type u
⊢ Function.Injective (@toDistrib R)

Tactic:
intro _ _ h

Result:
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocSemiring R
h : toDistrib = toDistrib
⊢ a₁✝ = a₂✝

Proof state:
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocSemiring R
h : toDistrib = toDistrib
⊢ a₁✝ = a₂✝

Tactic:
ext x y

Result:
case h_add.h.h
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocSemiring R
h : toDistrib = toDistrib
x y : R
⊢ x + y = x + y

case h_mul.h.h
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocSemiring R
h : toDistrib = toDistrib
x y : R
⊢ x * y = x * y
-- Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
@[to_additive]
lemma HasProd.of_nat_of_neg {f : ℤ → G} (hf₁ : HasProd (fun n : ℕ ↦ f n) g)
    (hf₂ : HasProd (fun n : ℕ ↦ f (-n)) g') : HasProd f (g * g' / f 0)

Proof state:
G : Type u_2
inst✝² : CommGroup G
g g' : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun n => f ↑n) g
hf₂ : HasProd (fun n => f (-↑n)) g'
⊢ HasProd (fun n => f (-(↑n + 1))) (g' / f 0)

Tactic:
rwa [← hasProd_nat_add_iff' 1, prod_range_one, Nat.cast_zero, neg_zero] at hf₂

Result:
no goals

Proof state:
G : Type u_2
inst✝² : CommGroup G
g g' : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun n => f ↑n) g
hf₂ : HasProd (fun n => f (-↑n)) g'
⊢ HasProd f (g * g' / f 0)

Tactic:
refine mul_div_assoc' g .. ▸ hf₁.of_nat_of_neg_add_one (m' := g' / f 0) ?_

Result:
G : Type u_2
inst✝² : CommGroup G
g g' : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun n => f ↑n) g
hf₂ : HasProd (fun n => f (-↑n)) g'
⊢ HasProd (fun n => f (-(↑n + 1))) (g' / f 0)
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem splits_of_exists_multiset {f : K[X]} {s : Multiset L}
    (hs : f.map i = C (i f.leadingCoeff) * (s.map fun a : L => X - C a).prod) : Splits i f :=
  letI := Classical.decEq K
  if hf0 : f = 0 then hf0.symm ▸ splits_zero i
  else
    Or.inr @fun p hp hdp => by
      rw [irreducible_iff_prime] at hp
      rw [hs, ← Multiset.prod_toList] at hdp
      obtain hd | hd := hp.2.2 _ _ hdp
      · refine (hp.2.1 <| isUnit_of_dvd_unit hd ?_).elim
        exact isUnit_C.2 ((leadingCoeff_ne_zero.2 hf0).isUnit.map i)
      · obtain ⟨q, hq, hd⟩ := hp.dvd_prod_iff.1 hd
        obtain ⟨a, _, rfl⟩ := Multiset.mem_map.1 (Multiset.mem_toList.1 hq)
        rw [degree_eq_degree_of_associated ((hp.dvd_prime_iff_associated <| prime_X_sub_C a).1 hd)]
        exact degree_X_sub_C a

Proof state:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
this : DecidableEq K := Classical.decEq K
hf0 : ¬f = 0
p : L[X]
hp : Irreducible p
hdp : p ∣ map i f
⊢ p.degree = 1

Tactic:
rw [irreducible_iff_prime] at hp

Result:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
this : DecidableEq K := Classical.decEq K
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ map i f
⊢ p.degree = 1
-- Mathlib/Topology/Bornology/Basic.lean
theorem isBounded_iUnion [Finite ι] {s : ι → Set α} :
    IsBounded (⋃ i, s i) ↔ ∀ i, IsBounded (s i)

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : Bornology α
inst✝ : Finite ι
s : ι → Set α
⊢ IsBounded (⋃ i, s i) ↔ ∀ (i : ι), IsBounded (s i)

Tactic:
rw [← sUnion_range, isBounded_sUnion (finite_range s), forall_mem_range]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem Finset.mulSupport_of_fiberwise_prod_subset_image [DecidableEq β] (s : Finset α) (f : α → M)
    (g : α → β) : (mulSupport fun b => (s.filter fun a => g a = b).prod f) ⊆ s.image g

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : b ∈ mulSupport fun b => (filter (fun a => g a = b) s).prod f
⊢ (filter (fun a => g a = b) s).Nonempty

Tactic:
exact Finset.nonempty_of_prod_ne_one h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
⊢ (mulSupport fun b => (filter (fun a => g a = b) s).prod f) ⊆ ↑(image g s)

Tactic:
simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, Function.support_subset_iff]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
⊢ (mulSupport fun b => (filter (fun a => g a = b) s).prod f) ⊆ g '' ↑s

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
⊢ (mulSupport fun b => (filter (fun a => g a = b) s).prod f) ⊆ g '' ↑s

Tactic:
intro b h

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : b ∈ mulSupport fun b => (filter (fun a => g a = b) s).prod f
⊢ b ∈ g '' ↑s

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : b ∈ mulSupport fun b => (filter (fun a => g a = b) s).prod f
this : (filter (fun a => g a = b) s).Nonempty
⊢ b ∈ g '' ↑s

Tactic:
simpa only [fiber_nonempty_iff_mem_image, Finset.mem_image, exists_prop]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : b ∈ mulSupport fun b => (filter (fun a => g a = b) s).prod f
⊢ b ∈ g '' ↑s

Tactic:
suffices (s.filter fun a : α => g a = b).Nonempty by
  simpa only [fiber_nonempty_iff_mem_image, Finset.mem_image, exists_prop]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : b ∈ mulSupport fun b => (filter (fun a => g a = b) s).prod f
⊢ (filter (fun a => g a = b) s).Nonempty
-- Mathlib/RingTheory/Smooth/Local.lean
theorem Algebra.FormallySmooth.iff_injective_lTensor_residueField {R S} [CommRing R]
    [CommRing S] [IsLocalRing S] [Algebra R S] (P : Algebra.Extension R S)
    [FormallySmooth R P.Ring]
    [Module.Free P.Ring (Ω[P.Ring⁄R])] [Module.Finite P.Ring (Ω[P.Ring⁄R])]
    (h' : P.ker.FG) :
    Algebra.FormallySmooth R S ↔
      Function.Injective (P.cotangentComplex.lTensor (ResidueField S))

Proof state:
R S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsLocalRing S
inst✝³ : Algebra R S
P : Extension R S
inst✝² : FormallySmooth R P.Ring
inst✝¹ : Module.Free P.Ring (Ω[P.Ring⁄R])
inst✝ : Module.Finite P.Ring (Ω[P.Ring⁄R])
h' : P.ker.FG
⊢ FormallySmooth R S ↔ Function.Injective ⇑(LinearMap.lTensor (ResidueField S) P.cotangentComplex)

Tactic:
have : Module.Finite P.Ring P.Cotangent :=
  have : Module.Finite P.Ring P.ker := ⟨(Submodule.fg_top _).mpr h'⟩
  .of_surjective _ Extension.Cotangent.mk_surjective

Result:
R S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsLocalRing S
inst✝³ : Algebra R S
P : Extension R S
inst✝² : FormallySmooth R P.Ring
inst✝¹ : Module.Free P.Ring (Ω[P.Ring⁄R])
inst✝ : Module.Finite P.Ring (Ω[P.Ring⁄R])
h' : P.ker.FG
this : Module.Finite P.Ring P.Cotangent
⊢ FormallySmooth R S ↔ Function.Injective ⇑(LinearMap.lTensor (ResidueField S) P.cotangentComplex)

Proof state:
R S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsLocalRing S
inst✝³ : Algebra R S
P : Extension R S
inst✝² : FormallySmooth R P.Ring
inst✝¹ : Module.Free P.Ring (Ω[P.Ring⁄R])
inst✝ : Module.Finite P.Ring (Ω[P.Ring⁄R])
h' : P.ker.FG
this : Module.Finite P.Ring P.Cotangent
⊢ FormallySmooth R S ↔ Function.Injective ⇑(LinearMap.lTensor (ResidueField S) P.cotangentComplex)

Tactic:
have : Module.Finite S P.Cotangent := Module.Finite.of_restrictScalars_finite P.Ring _ _

Result:
R S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsLocalRing S
inst✝³ : Algebra R S
P : Extension R S
inst✝² : FormallySmooth R P.Ring
inst✝¹ : Module.Free P.Ring (Ω[P.Ring⁄R])
inst✝ : Module.Finite P.Ring (Ω[P.Ring⁄R])
h' : P.ker.FG
this✝ : Module.Finite P.Ring P.Cotangent
this : Module.Finite S P.Cotangent
⊢ FormallySmooth R S ↔ Function.Injective ⇑(LinearMap.lTensor (ResidueField S) P.cotangentComplex)

Proof state:
R S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsLocalRing S
inst✝³ : Algebra R S
P : Extension R S
inst✝² : FormallySmooth R P.Ring
inst✝¹ : Module.Free P.Ring (Ω[P.Ring⁄R])
inst✝ : Module.Finite P.Ring (Ω[P.Ring⁄R])
h' : P.ker.FG
this✝ : Module.Finite P.Ring P.Cotangent
this : Module.Finite S P.Cotangent
⊢ FormallySmooth R S ↔ Function.Injective ⇑(LinearMap.lTensor (ResidueField S) P.cotangentComplex)

Tactic:
rw [← IsLocalRing.split_injective_iff_lTensor_residueField_injective,
  P.formallySmooth_iff_split_injection]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
@[simp] lemma abs_arg_inv (x : ℂ) : |x⁻¹.arg| = |x.arg|

Proof state:
x : ℂ
⊢ |x⁻¹.arg| = |x.arg|

Tactic:
rw [arg_inv]

Result:
x : ℂ
⊢ |if x.arg = π then π else -x.arg| = |x.arg|

Proof state:
x : ℂ
⊢ |if x.arg = π then π else -x.arg| = |x.arg|

Tactic:
split_ifs <;> simp [*]

Result:
no goals