harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem factorization_zero : factorization 0 = 0

Proof state:
⊢ factorization 0 = 0

Tactic:
ext

Result:
case h
a✝ : ℕ
⊢ (factorization 0) a✝ = 0 a✝

Proof state:
case h
a✝ : ℕ
⊢ (factorization 0) a✝ = 0 a✝

Tactic:
simp [factorization]

Result:
no goals
-- Mathlib/Algebra/Algebra/Basic.lean
theorem map_mul_algebraMap (f : A →ₗ[R] B) (a : A) (r : R) :
    f (a * algebraMap R A r) = f a * algebraMap R B r

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
a : A
r : R
⊢ f (a * (algebraMap R A) r) = f a * (algebraMap R B) r

Tactic:
rw [← Algebra.commutes, ← Algebra.commutes, map_algebraMap_mul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.degree_map [Semiring S] [Nontrivial S] {P : R[X]} (hmo : P.Monic) (f : R →+* S) :
    (P.map f).degree = P.degree

Proof state:
case neg
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
hP : ¬P = 0
⊢ P.degree ≤ (Polynomial.map f P).degree

Tactic:
rw [degree_eq_natDegree hP]

Result:
case neg
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
hP : ¬P = 0
⊢ ↑P.natDegree ≤ (Polynomial.map f P).degree

Proof state:
case neg
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
hP : ¬P = 0
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
case pos
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
hP : P = 0
⊢ (Polynomial.map f P).degree = P.degree

Tactic:
simp [hP]

Result:
no goals

Proof state:
case neg
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
hP : ¬P = 0
⊢ (Polynomial.map f P).coeff P.natDegree ≠ 0

Tactic:
rw [coeff_map, Monic.coeff_natDegree hmo, RingHom.map_one]

Result:
case neg
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
hP : ¬P = 0
⊢ 1 ≠ 0

Proof state:
case neg
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
hP : ¬P = 0
⊢ (Polynomial.map f P).degree = P.degree

Tactic:
refine le_antisymm degree_map_le ?_

Result:
case neg
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
hP : ¬P = 0
⊢ P.degree ≤ (Polynomial.map f P).degree

Proof state:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ (Polynomial.map f P).degree = P.degree

Tactic:
by_cases hP : P = 0

Result:
case pos
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
hP : P = 0
⊢ (Polynomial.map f P).degree = P.degree

case neg
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
hP : ¬P = 0
⊢ (Polynomial.map f P).degree = P.degree

Proof state:
case neg
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
hP : ¬P = 0
⊢ ↑P.natDegree ≤ (Polynomial.map f P).degree

Tactic:
refine le_degree_of_ne_zero ?_

Result:
case neg
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
hP : ¬P = 0
⊢ (Polynomial.map f P).coeff P.natDegree ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head?_concat {a : α} : (l ++ [a]).head? = l.head?.getD a

Proof state:
α : Type u_1
l : List α
a : α
⊢ (l ++ [a]).head? = some (l.head?.getD a)

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_modify [LawfulBEq α] {k k' : α} {f : β k → β k}
    (h : m.WF) {hc : k' ∈ m.modify k f} :
    (m.modify k f).get k' hc =
     if heq : k == k' then
       haveI h' : k ∈ m := mem_congr h heq |>.mpr <| mem_modify h |>.mp hc
       cast (congrArg β (eq_of_beq heq)) <| f (m.get k h')
     else
       haveI h' : k' ∈ m := mem_modify h |>.mp hc
       m.get k' h'

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : β k → β k
h : m.WF
hc : k' ∈ m.modify k f
⊢ (m.modify k f).contains k' = true →
    (m.modify k f).get k' hc = if heq : (k == k') = true then cast ⋯ (f (m.get k ⋯)) else m.get k' ⋯

Tactic:
simp_to_raw using Raw₀.get_modify

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : β k → β k
h : m.WF
hc✝ : k' ∈ m.modify k f
hc : (m.modify k f).contains k' = true
⊢ (m.modify k f).get k' hc✝ = if heq : (k == k') = true then cast ⋯ (f (m.get k ⋯)) else m.get k' ⋯

Tactic:
revert hc

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : β k → β k
h : m.WF
hc : k' ∈ m.modify k f
⊢ (m.modify k f).contains k' = true →
    (m.modify k f).get k' hc = if heq : (k == k') = true then cast ⋯ (f (m.get k ⋯)) else m.get k' ⋯

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : β k → β k
h : m.WF
hc : k' ∈ m.modify k f
⊢ (m.modify k f).get k' hc = if heq : (k == k') = true then cast ⋯ (f (m.get k ⋯)) else m.get k' ⋯

Tactic:
simp only [mem_iff_contains] at hc

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : β k → β k
h : m.WF
hc✝ : k' ∈ m.modify k f
hc : (m.modify k f).contains k' = true
⊢ (m.modify k f).get k' hc✝ = if heq : (k == k') = true then cast ⋯ (f (m.get k ⋯)) else m.get k' ⋯
-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
theorem IsStableUnderBaseChange.pullback_fst_appTop
    (hP : IsStableUnderBaseChange P) (hP' : RespectsIso P)
    {X Y S : Scheme} [IsAffine X] [IsAffine Y] [IsAffine S] (f : X ⟶ S) (g : Y ⟶ S)
    (H : P g.appTop.hom) : P (pullback.fst f g).appTop.hom

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y S : Scheme
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appTop (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g))))

Tactic:
have := congr_arg Quiver.Hom.unop
    (PreservesPullback.iso_hom_fst AffineScheme.Γ.rightOp (AffineScheme.ofHom f)
      (AffineScheme.ofHom g))

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y S : Scheme
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
this :
  ((PreservesPullback.iso AffineScheme.Γ.rightOp (AffineScheme.ofHom f) (AffineScheme.ofHom g)).hom ≫
        pullback.fst (AffineScheme.Γ.rightOp.map (AffineScheme.ofHom f))
          (AffineScheme.Γ.rightOp.map (AffineScheme.ofHom g))).unop =
    (AffineScheme.Γ.rightOp.map (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g))).unop
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appTop (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g))))
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem rank_eq_one (v : M) (n : v ≠ 0) (h : ∀ w : M, ∃ c : R, c • v = w) :
    Module.rank R M = 1

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : StrongRankCondition R
v : M
n : v ≠ 0
h : ∀ (w : M), ∃ c, c • v = w
⊢ Module.rank R M = 1

Tactic:
haveI := nontrivial_of_invariantBasisNumber R

Result:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : StrongRankCondition R
v : M
n : v ≠ 0
h : ∀ (w : M), ∃ c, c • v = w
this : Nontrivial R
⊢ Module.rank R M = 1

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : StrongRankCondition R
v : M
n : v ≠ 0
h : ∀ (w : M), ∃ c, c • v = w
this : Nontrivial R
⊢ Module.rank R M = 1

Tactic:
obtain ⟨b⟩ := (Basis.basis_singleton_iff.{_, _, u} PUnit).mpr ⟨v, n, h⟩

Result:
case intro
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : StrongRankCondition R
v : M
n : v ≠ 0
h : ∀ (w : M), ∃ c, c • v = w
this : Nontrivial R
b : Basis PUnit.{u + 1} R M
⊢ Module.rank R M = 1

Proof state:
case intro
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : StrongRankCondition R
v : M
n : v ≠ 0
h : ∀ (w : M), ∃ c, c • v = w
this : Nontrivial R
b : Basis PUnit.{u + 1} R M
⊢ Module.rank R M = 1

Tactic:
rw [rank_eq_card_basis b, Fintype.card_punit, Nat.cast_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivMod.lean
theorem ofNat_fdiv : ∀ m n : Nat, ↑(m / n) = fdiv ↑m ↑n
  | 0, _ => by simp [fdiv]
  | succ _, _ => rfl

Proof state:
x✝ : Nat
⊢ ↑(0 / x✝) = (↑0).fdiv ↑x✝

Tactic:
simp [fdiv]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Split.lean
theorem ext (A₁ A₂ : IndexSet Δ) (h₁ : A₁.1 = A₂.1) (h₂ : A₁.e ≫ eqToHom (by rw [h₁]) = A₂.e) :
    A₁ = A₂

Proof state:
case mk.mk
Δ : SimplexCategoryᵒᵖ
A₂ : IndexSet Δ
Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
h₁ : ⟨Δ₁, ⟨α₁, hα₁⟩⟩.fst = A₂.fst
h₂ : e ⟨Δ₁, ⟨α₁, hα₁⟩⟩ ≫ eqToHom ⋯ = A₂.e
⊢ ⟨Δ₁, ⟨α₁, hα₁⟩⟩ = A₂

Tactic:
rcases A₂ with ⟨Δ₂, ⟨α₂, hα₂⟩⟩

Result:
case mk.mk.mk.mk
Δ Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
Δ₂ : SimplexCategoryᵒᵖ
α₂ : unop Δ ⟶ unop Δ₂
hα₂ : Epi α₂
h₁ : ⟨Δ₁, ⟨α₁, hα₁⟩⟩.fst = ⟨Δ₂, ⟨α₂, hα₂⟩⟩.fst
h₂ : e ⟨Δ₁, ⟨α₁, hα₁⟩⟩ ≫ eqToHom ⋯ = e ⟨Δ₂, ⟨α₂, hα₂⟩⟩
⊢ ⟨Δ₁, ⟨α₁, hα₁⟩⟩ = ⟨Δ₂, ⟨α₂, hα₂⟩⟩

Proof state:
case mk.mk.mk.mk
Δ Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
α₂ : unop Δ ⟶ unop Δ₁
hα₂ : Epi α₂
h₂ : e ⟨Δ₁, ⟨α₁, hα₁⟩⟩ ≫ eqToHom ⋯ = e ⟨Δ₁, ⟨α₂, hα₂⟩⟩
⊢ ⟨Δ₁, ⟨α₁, hα₁⟩⟩ = ⟨Δ₁, ⟨α₂, hα₂⟩⟩

Tactic:
simp only [eqToHom_refl, comp_id, IndexSet.e] at h₂

Result:
case mk.mk.mk.mk
Δ Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
α₂ : unop Δ ⟶ unop Δ₁
hα₂ : Epi α₂
h₂ : α₁ = α₂
⊢ ⟨Δ₁, ⟨α₁, hα₁⟩⟩ = ⟨Δ₁, ⟨α₂, hα₂⟩⟩

Proof state:
Δ : SimplexCategoryᵒᵖ
A₁ A₂ : IndexSet Δ
h₁ : A₁.fst = A₂.fst
h₂ : A₁.e ≫ eqToHom ⋯ = A₂.e
⊢ A₁ = A₂

Tactic:
rcases A₁ with ⟨Δ₁, ⟨α₁, hα₁⟩⟩

Result:
case mk.mk
Δ : SimplexCategoryᵒᵖ
A₂ : IndexSet Δ
Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
h₁ : ⟨Δ₁, ⟨α₁, hα₁⟩⟩.fst = A₂.fst
h₂ : e ⟨Δ₁, ⟨α₁, hα₁⟩⟩ ≫ eqToHom ⋯ = A₂.e
⊢ ⟨Δ₁, ⟨α₁, hα₁⟩⟩ = A₂

Proof state:
case mk.mk.mk.mk
Δ Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
α₂ : unop Δ ⟶ unop Δ₁
hα₂ : Epi α₂
h₂ : α₁ = α₂
⊢ ⟨Δ₁, ⟨α₁, hα₁⟩⟩ = ⟨Δ₁, ⟨α₂, hα₂⟩⟩

Tactic:
simp only [h₂]

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{?u.853, u_1} C
Δ : SimplexCategoryᵒᵖ
A A₁ A₂ : IndexSet Δ
h₁ : A₁.fst = A₂.fst
⊢ unop A₁.fst = unop A₂.fst

Tactic:
rw [h₁]

Result:
no goals

Proof state:
case mk.mk.mk.mk
Δ Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
Δ₂ : SimplexCategoryᵒᵖ
α₂ : unop Δ ⟶ unop Δ₂
hα₂ : Epi α₂
h₁ : Δ₁ = Δ₂
h₂ : e ⟨Δ₁, ⟨α₁, hα₁⟩⟩ ≫ eqToHom ⋯ = e ⟨Δ₂, ⟨α₂, hα₂⟩⟩
⊢ ⟨Δ₁, ⟨α₁, hα₁⟩⟩ = ⟨Δ₂, ⟨α₂, hα₂⟩⟩

Tactic:
subst h₁

Result:
case mk.mk.mk.mk
Δ Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
α₂ : unop Δ ⟶ unop Δ₁
hα₂ : Epi α₂
h₂ : e ⟨Δ₁, ⟨α₁, hα₁⟩⟩ ≫ eqToHom ⋯ = e ⟨Δ₁, ⟨α₂, hα₂⟩⟩
⊢ ⟨Δ₁, ⟨α₁, hα₁⟩⟩ = ⟨Δ₁, ⟨α₂, hα₂⟩⟩

Proof state:
case mk.mk.mk.mk
Δ Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
Δ₂ : SimplexCategoryᵒᵖ
α₂ : unop Δ ⟶ unop Δ₂
hα₂ : Epi α₂
h₁ : ⟨Δ₁, ⟨α₁, hα₁⟩⟩.fst = ⟨Δ₂, ⟨α₂, hα₂⟩⟩.fst
h₂ : e ⟨Δ₁, ⟨α₁, hα₁⟩⟩ ≫ eqToHom ⋯ = e ⟨Δ₂, ⟨α₂, hα₂⟩⟩
⊢ ⟨Δ₁, ⟨α₁, hα₁⟩⟩ = ⟨Δ₂, ⟨α₂, hα₂⟩⟩

Tactic:
simp only at h₁

Result:
case mk.mk.mk.mk
Δ Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
Δ₂ : SimplexCategoryᵒᵖ
α₂ : unop Δ ⟶ unop Δ₂
hα₂ : Epi α₂
h₁ : Δ₁ = Δ₂
h₂ : e ⟨Δ₁, ⟨α₁, hα₁⟩⟩ ≫ eqToHom ⋯ = e ⟨Δ₂, ⟨α₂, hα₂⟩⟩
⊢ ⟨Δ₁, ⟨α₁, hα₁⟩⟩ = ⟨Δ₂, ⟨α₂, hα₂⟩⟩
-- Mathlib/NumberTheory/Dioph.lean
theorem reindex_diophFn {f : (α → ℕ) → ℕ} (g : α → β) (d : DiophFn f) :
    DiophFn fun v => f (v ∘ g)

Proof state:
α β : Type u
f : (α → ℕ) → ℕ
g : α → β
d : DiophFn f
⊢ DiophFn fun v => f (v ∘ g)

Tactic:
convert reindex_dioph (Option β) (Option.map g) d

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem Prime.prod_divisors {α : Type*} [CommMonoid α] {p : ℕ} {f : ℕ → α} (h : p.Prime) :
    ∏ x ∈ p.divisors, f x = f p * f 1

Proof state:
α : Type u_1
inst✝ : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x ∈ p.divisors, f x = f p * f 1

Tactic:
rw [← cons_self_properDivisors h.ne_zero, prod_cons, h.prod_properDivisors]

Result:
no goals
-- Mathlib/Algebra/Small/Group.lean
@[to_additive (attr := simp)]
lemma equivShrink_div [Div α] [Small α] (x y : α) :
    equivShrink α (x / y) = equivShrink α x / equivShrink α y

Proof state:
α : Type u_1
inst✝¹ : Div α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ (equivShrink α) (x / y) =
    (equivShrink α).symm.symm ((equivShrink α).symm ((equivShrink α) x) / (equivShrink α).symm ((equivShrink α) y))

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Div α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ (equivShrink α) (x / y) = (equivShrink α) x / (equivShrink α) y

Tactic:
rw [Equiv.div_def]

Result:
α : Type u_1
inst✝¹ : Div α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ (equivShrink α) (x / y) =
    (equivShrink α).symm.symm ((equivShrink α).symm ((equivShrink α) x) / (equivShrink α).symm ((equivShrink α) y))
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_add_intCast (hx : x ≠ 0) (y : ℝ) (n : ℤ) : x ^ (y + n) = x ^ y * x ^ n

Proof state:
case a
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)

Tactic:
exact Real.rpow_add_intCast (mod_cast hx) _ _

Result:
no goals

Proof state:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
ext

Result:
case a
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma add_of_Y_ne {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) (hy : P y * Q z ≠ Q y * P z) :
    W.add P Q = addU P Q • ![0, 1, 0]

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ Q y * P z
⊢ W.add P Q = addU P Q • ![0, 1, 0]

Tactic:
rw [add, if_neg <| not_equiv_of_Y_ne hy, addXYZ_of_X_eq hP hQ hPz hQz hx]

Result:
no goals
-- Mathlib/RingTheory/PiTensorProduct.lean
protected lemma mul_one (x : ⨂[R] i, A i) : mul x (tprod R 1) = x

Proof state:
case add
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonAssocSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
x✝ y✝ : ⨂[R] (i : ι), A i
h1 : (mul x✝) ((tprod R) 1) = x✝
h2 : (mul y✝) ((tprod R) 1) = y✝
⊢ (mul (x✝ + y✝)) ((tprod R) 1) = x✝ + y✝

Tactic:
simp [h1, h2]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonAssocSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
x : ⨂[R] (i : ι), A i
⊢ (mul x) ((tprod R) 1) = x

Tactic:
induction x using PiTensorProduct.induction_on with
| smul_tprod => simp
| add _ _ h1 h2 => simp [h1, h2]

Result:
no goals

Proof state:
case smul_tprod
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonAssocSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
r✝ : R
f✝ : (i : ι) → A i
⊢ (mul (r✝ • (tprod R) f✝)) ((tprod R) 1) = r✝ • (tprod R) f✝

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_neg_of_lt_zero (h0 : x < 0) (h1 : -1 < x) : log x < 0

Proof state:
x : ℝ
h0 : x < 0
h1 : -1 < x
⊢ log x < 0

Tactic:
rw [← neg_neg x, log_neg_eq_log]

Result:
x : ℝ
h0 : x < 0
h1 : -1 < x
⊢ log (-x) < 0

Proof state:
x : ℝ
h0 : x < 0
h1 : -1 < x
⊢ 0 < -x

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
h0 : x < 0
h1 : -1 < x
⊢ log (-x) < 0

Tactic:
have h0' : 0 < -x := by linarith

Result:
x : ℝ
h0 : x < 0
h1 : -1 < x
h0' : 0 < -x
⊢ log (-x) < 0

Proof state:
x : ℝ
h0 : x < 0
h1 : -1 < x
h0' : 0 < -x
⊢ -x < 1

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
h0 : x < 0
h1 : -1 < x
h0' : 0 < -x
⊢ log (-x) < 0

Tactic:
have h1' : -x < 1 := by linarith

Result:
x : ℝ
h0 : x < 0
h1 : -1 < x
h0' : 0 < -x
h1' : -x < 1
⊢ log (-x) < 0

Proof state:
x : ℝ
h0 : x < 0
h1 : -1 < x
h0' : 0 < -x
h1' : -x < 1
⊢ log (-x) < 0

Tactic:
exact log_neg h0' h1'

Result:
no goals
-- Mathlib/Data/Matrix/Diagonal.lean
theorem diagonal_apply_ne [Zero α] (d : n → α) {i j : n} (h : i ≠ j) : (diagonal d) i j = 0

Proof state:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
d : n → α
i j : n
h : i ≠ j
⊢ diagonal d i j = 0

Tactic:
simp [diagonal, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/List.lean
theorem forIn_some [Monad m] [LawfulMonad m] (a : α) (b : β) (f : α → β → m (ForInStep β)) :
    forIn (some a) b f = bind (f a b) (fun r => pure (ForInStep.value r))

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
b : β
f : α → β → m (ForInStep β)
⊢ (do
      let __do_lift ← f a b
      match __do_lift with
        | ForInStep.done r => pure r
        | ForInStep.yield r => pure r) =
    ForInStep.value <$> f a b

Tactic:
rw [map_eq_pure_bind]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
b : β
f : α → β → m (ForInStep β)
⊢ (do
      let __do_lift ← f a b
      match __do_lift with
        | ForInStep.done r => pure r
        | ForInStep.yield r => pure r) =
    do
    let a ← f a b
    pure a.value

Proof state:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
b : β
f : α → β → m (ForInStep β)
x : ForInStep β
⊢ (match x with
    | ForInStep.done r => pure r
    | ForInStep.yield r => pure r) =
    pure x.value

Tactic:
split <;> rfl

Result:
no goals

Proof state:
case e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
b : β
f : α → β → m (ForInStep β)
⊢ (fun __do_lift =>
      match __do_lift with
      | ForInStep.done r => pure r
      | ForInStep.yield r => pure r) =
    fun a => pure a.value

Tactic:
funext x

Result:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
b : β
f : α → β → m (ForInStep β)
x : ForInStep β
⊢ (match x with
    | ForInStep.done r => pure r
    | ForInStep.yield r => pure r) =
    pure x.value

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
b : β
f : α → β → m (ForInStep β)
⊢ (do
      let __do_lift ← f a b
      match __do_lift with
        | ForInStep.done r => pure r
        | ForInStep.yield r => pure r) =
    do
    let a ← f a b
    pure a.value

Tactic:
congr

Result:
case e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
b : β
f : α → β → m (ForInStep β)
⊢ (fun __do_lift =>
      match __do_lift with
      | ForInStep.done r => pure r
      | ForInStep.yield r => pure r) =
    fun a => pure a.value

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
b : β
f : α → β → m (ForInStep β)
⊢ forIn (some a) b f = do
    let r ← f a b
    pure r.value

Tactic:
simp only [forIn, forIn', bind_pure_comp]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
b : β
f : α → β → m (ForInStep β)
⊢ (do
      let __do_lift ← f a b
      match __do_lift with
        | ForInStep.done r => pure r
        | ForInStep.yield r => pure r) =
    ForInStep.value <$> f a b
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem csSup_eq_univ_of_not_bddAbove {s : Set α} (hs : ¬BddAbove s) : sSup s = sSup univ

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : BddAbove univ
⊢ BddAbove s

Tactic:
exact hs.mono (subset_univ _)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ sSup s = sSup univ

Tactic:
rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (s := univ)]

Result:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ ¬BddAbove univ

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ ¬BddAbove univ

Tactic:
contrapose! hs

Result:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : BddAbove univ
⊢ BddAbove s
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addU_smul {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0) {u v : F} (hu : u ≠ 0)
    (hv : v ≠ 0) : addU (u • P) (v • Q) = (u * v) ^ 2 * addU P Q

Proof state:
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
u v : F
hu : u ≠ 0
hv : v ≠ 0
⊢ addU (u • P) (v • Q) = (u * v) ^ 2 * addU P Q

Tactic:
field_simp [addU, smul_fin3_ext]

Result:
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
u v : F
hu : u ≠ 0
hv : v ≠ 0
⊢ (v ^ 3 * Q y * (u * P z) ^ 3 - u ^ 3 * P y * (v * Q z) ^ 3) * (P z * Q z) =
    (u * v) ^ 2 * (Q y * P z ^ 3 - P y * Q z ^ 3) * (u * P z * (v * Q z))

Proof state:
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
u v : F
hu : u ≠ 0
hv : v ≠ 0
⊢ (v ^ 3 * Q y * (u * P z) ^ 3 - u ^ 3 * P y * (v * Q z) ^ 3) * (P z * Q z) =
    (u * v) ^ 2 * (Q y * P z ^ 3 - P y * Q z ^ 3) * (u * P z * (v * Q z))

Tactic:
ring1

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
protected lemma comp_add {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (z₂ z₂' : Cochain G K n₂)
    (h : n₁ + n₂ = n₁₂) : z₁.comp (z₂ + z₂') h = z₁.comp z₂ h + z₁.comp z₂' h

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ z₂' : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ p + n₁ + n₂ = q

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ z₂' : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ z₁.comp (z₂ + z₂') h = z₁.comp z₂ h + z₁.comp z₂' h

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ z₂' : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ (z₁.comp (z₂ + z₂') h).v p q hpq = (z₁.comp z₂ h + z₁.comp z₂' h).v p q hpq

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ z₂' : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ (z₁.comp (z₂ + z₂') h).v p q hpq = (z₁.comp z₂ h + z₁.comp z₂' h).v p q hpq

Tactic:
simp only [comp_v _ _ h p _ q rfl (by omega), add_v, comp_add]

Result:
no goals