harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem even_card_iff_char_two : ringChar F = 2 ↔ Fintype.card F % 2 = 0

Proof state:
case intro.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = 2 ↔ ringChar F = 2 ∧ ↑n ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = 2 ↔ Fintype.card F % 2 = 0

Tactic:
rw [h, ← Nat.even_iff, Nat.even_pow, hp.even_iff]

Result:
case intro.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = 2 ↔ ringChar F = 2 ∧ ↑n ≠ 0

Proof state:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
⊢ ringChar F = 2 ↔ Fintype.card F % 2 = 0

Tactic:
rcases FiniteField.card F (ringChar F) with ⟨n, hp, h⟩

Result:
case intro.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = 2 ↔ Fintype.card F % 2 = 0
-- Mathlib/CategoryTheory/Sites/Over.lean
lemma overEquiv_le_overEquiv_iff {X : C} {Y : Over X} (R₁ R₂ : Sieve Y) :
    R₁.overEquiv Y ≤ R₂.overEquiv Y ↔ R₁ ≤ R₂

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R₁ R₂ : Sieve Y
⊢ (overEquiv Y) R₁ ≤ (overEquiv Y) R₂ ↔ R₁ ≤ R₂

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Sieve.functorPushforward_monotone _ _ h⟩

Result:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R₁ R₂ : Sieve Y
h : (overEquiv Y) R₁ ≤ (overEquiv Y) R₂
⊢ R₁ ≤ R₂

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R₁ R₂ : Sieve Y
h : (overEquiv Y).symm ((overEquiv Y) R₁) ≤ (overEquiv Y).symm ((overEquiv Y) R₂)
⊢ R₁ ≤ R₂

Tactic:
simpa using h

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R₁ R₂ : Sieve Y
h : (overEquiv Y) R₁ ≤ (overEquiv Y) R₂
⊢ R₁ ≤ R₂

Tactic:
replace h : (overEquiv Y).symm (R₁.overEquiv Y) ≤ (overEquiv Y).symm (R₂.overEquiv Y) :=
  Sieve.functorPullback_monotone _ _ h

Result:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R₁ R₂ : Sieve Y
h : (overEquiv Y).symm ((overEquiv Y) R₁) ≤ (overEquiv Y).symm ((overEquiv Y) R₂)
⊢ R₁ ≤ R₂
-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem eq_orthocenter_of_forall_mem_altitude {t : Triangle ℝ P} {i₁ i₂ : Fin 3} {p : P}
    (h₁₂ : i₁ ≠ i₂) (h₁ : p ∈ t.altitude i₁) (h₂ : p ∈ t.altitude i₂) : p = t.orthocenter

Proof state:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
i₃ : Fin 3
h₂ : p ∈ mongePlane t i₃ i₁
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
hi : i₃ ≠ i₁
⊢ p ∈ mongePlane t i₃ i₁

case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
i₃ : Fin 3
h₂ : p ∈ mongePlane t i₃ i₁
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
hi : i₃ ≠ i₂
⊢ p ∈ mongePlane t i₃ i₂

Tactic:
all_goals assumption

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
@[reassoc]
lemma naturality_φ₁ (f : S₁ ⟶ S₂) : S₁.φ₁ ≫ f.f₂.τ₁ = functorP.map f ≫ S₂.φ₁

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ S₁.φ₁ ≫ f.f₂.τ₁ = functorP.map f ≫ S₂.φ₁

Tactic:
simp only [← cancel_mono S₂.L₂.f, assoc, φ₁_L₂_f, ← naturality_φ₂, f.f₂.comm₁₂, φ₁_L₂_f_assoc]

Result:
no goals
-- Mathlib/Control/LawfulFix.lean
theorem fix_le {X : (a : _) → Part <| β a} (hX : f X ≤ X) : Part.fix f ≤ X

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
⊢ Part.fix ⇑f ≤ X

Tactic:
rw [fix_eq_ωSup f]

Result:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
⊢ ωSup (approxChain f) ≤ X

Proof state:
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
⊢ { toFun := approx ⇑f, monotone' := ⋯ } 0 ≤ X

Tactic:
apply bot_le

Result:
no goals

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
n✝ : ℕ
i_ih : { toFun := approx ⇑f, monotone' := ⋯ } n✝ ≤ X
⊢ { toFun := approx ⇑f, monotone' := ⋯ } (n✝ + 1) ≤ f X

Tactic:
apply f.monotone i_ih

Result:
no goals

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
⊢ ωSup (approxChain f) ≤ X

Tactic:
apply ωSup_le _ _ _

Result:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
⊢ ∀ (i : ℕ), (approxChain f) i ≤ X

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
⊢ ∀ (i : ℕ), (approxChain f) i ≤ X

Tactic:
simp only [Fix.approxChain, OrderHom.coe_mk]

Result:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
⊢ ∀ (i : ℕ), { toFun := approx ⇑f, monotone' := ⋯ } i ≤ X

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
⊢ ∀ (i : ℕ), { toFun := approx ⇑f, monotone' := ⋯ } i ≤ X

Tactic:
intro i

Result:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
i : ℕ
⊢ { toFun := approx ⇑f, monotone' := ⋯ } i ≤ X

Proof state:
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
n✝ : ℕ
i_ih : { toFun := approx ⇑f, monotone' := ⋯ } n✝ ≤ X
⊢ { toFun := approx ⇑f, monotone' := ⋯ } (n✝ + 1) ≤ X

Tactic:
trans f X

Result:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
n✝ : ℕ
i_ih : { toFun := approx ⇑f, monotone' := ⋯ } n✝ ≤ X
⊢ { toFun := approx ⇑f, monotone' := ⋯ } (n✝ + 1) ≤ f X

α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
n✝ : ℕ
i_ih : { toFun := approx ⇑f, monotone' := ⋯ } n✝ ≤ X
⊢ f X ≤ X

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
n✝ : ℕ
i_ih : { toFun := approx ⇑f, monotone' := ⋯ } n✝ ≤ X
⊢ f X ≤ X

Tactic:
apply hX

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem AffineIndependent.mem_affineSpan_iff [Nontrivial k] {p : ι → P}
    (ha : AffineIndependent k p) (i : ι) (s : Set ι) : p i ∈ affineSpan k (p '' s) ↔ i ∈ s

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i : ι
s : Set ι
⊢ p i ∈ affineSpan k (p '' s) ↔ i ∈ s

Tactic:
constructor

Result:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i : ι
s : Set ι
⊢ p i ∈ affineSpan k (p '' s) → i ∈ s

case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i : ι
s : Set ι
⊢ i ∈ s → p i ∈ affineSpan k (p '' s)

Proof state:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i : ι
s : Set ι
hs : p i ∈ affineSpan k (p '' s)
⊢ i ∈ s

Tactic:
have h :=
  AffineIndependent.exists_mem_inter_of_exists_mem_inter_affineSpan ha hs
    (mem_affineSpan k (Set.mem_image_of_mem _ (Set.mem_singleton _)))

Result:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i : ι
s : Set ι
hs : p i ∈ affineSpan k (p '' s)
h : ∃ i_1, i_1 ∈ s ∩ {i}
⊢ i ∈ s

Proof state:
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i : ι
s : Set ι
⊢ i ∈ s → p i ∈ affineSpan k (p '' s)

Tactic:
exact fun h => mem_affineSpan k (Set.mem_image_of_mem p h)

Result:
no goals

Proof state:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i : ι
s : Set ι
hs : p i ∈ affineSpan k (p '' s)
h : ∃ i_1, i_1 ∈ s ∩ {i}
⊢ i ∈ s

Tactic:
rwa [← Set.nonempty_def, Set.inter_singleton_nonempty] at h

Result:
no goals

Proof state:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i : ι
s : Set ι
⊢ p i ∈ affineSpan k (p '' s) → i ∈ s

Tactic:
intro hs

Result:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i : ι
s : Set ι
hs : p i ∈ affineSpan k (p '' s)
⊢ i ∈ s
-- Mathlib/Algebra/Group/Fin/Tuple.lean
@[simp] lemma cons_eq_zero_iff {v : Fin n → α} {x : α} : vecCons x v = 0 ↔ x = 0 ∧ v = 0 where
  mp h := ⟨congr_fun h 0, by convert congr_arg vecTail h⟩
  mpr := fun ⟨hx, hv⟩ ↦ by simp [hx, hv]

Proof state:
α : Type u_1
n : ℕ
inst✝ : Zero α
v : Fin n → α
x : α
x✝ : x = 0 ∧ v = 0
hx : x = 0
hv : v = 0
⊢ vecCons x v = 0

Tactic:
simp [hx, hv]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
inst✝ : Zero α
v : Fin n → α
x : α
h : vecCons x v = 0
⊢ v = 0

Tactic:
convert congr_arg vecTail h

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Turan.lean
/-- In a Turán-maximal graph, non-adjacency is transitive. -/
lemma not_adj_trans (h : G.IsTuranMaximal r) (hts : ¬G.Adj t s) (hsu : ¬G.Adj s u) :
    ¬G.Adj t u

Proof state:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
h : G.IsTuranMaximal r
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
⊢ ¬G.Adj t u

Tactic:
have dst := h.degree_eq_of_not_adj hst

Result:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
h : G.IsTuranMaximal r
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
⊢ ¬G.Adj t u
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem monic_multiset_prod_of_monic (t : Multiset ι) (f : ι → R[X]) (ht : ∀ i ∈ t, Monic (f i)) :
    Monic (t.map f).prod

Proof state:
case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.Monic
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (f a * (Multiset.map f t).prod).Monic

Tactic:
exact (ht _ (Multiset.mem_cons_self _ _)).mul (ih fun _ hi => ht _ (Multiset.mem_cons_of_mem hi))

Result:
no goals

Proof state:
case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.Monic
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (Multiset.map f (a ::ₘ t)).prod.Monic

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons]

Result:
case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.Monic
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (f a * (Multiset.map f t).prod).Monic

Proof state:
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
ht : ∀ i ∈ t, (f i).Monic
⊢ (Multiset.map f t).prod.Monic

Tactic:
revert ht

Result:
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.Monic

Proof state:
case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ ∀ (a : ι) (s : Multiset ι),
    ((∀ i ∈ s, (f i).Monic) → (Multiset.map f s).prod.Monic) →
      (∀ i ∈ a ::ₘ s, (f i).Monic) → (Multiset.map f (a ::ₘ s)).prod.Monic

Tactic:
intro a t ih ht

Result:
case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.Monic
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (Multiset.map f (a ::ₘ t)).prod.Monic

Proof state:
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.Monic

Tactic:
refine t.induction_on ?_ ?_

Result:
case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (∀ i ∈ 0, (f i).Monic) → (Multiset.map f 0).prod.Monic

case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ ∀ (a : ι) (s : Multiset ι),
    ((∀ i ∈ s, (f i).Monic) → (Multiset.map f s).prod.Monic) →
      (∀ i ∈ a ::ₘ s, (f i).Monic) → (Multiset.map f (a ::ₘ s)).prod.Monic

Proof state:
case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (∀ i ∈ 0, (f i).Monic) → (Multiset.map f 0).prod.Monic

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem mk_le {f g : CauSeq ℚ abs} : mk f ≤ mk g ↔ f ≤ g

Proof state:
f g : CauSeq ℚ abs
⊢ f < g ∨ f ≈ g ↔ f ≤ g

Tactic:
rfl

Result:
no goals

Proof state:
f g : CauSeq ℚ abs
⊢ mk f ≤ mk g ↔ f ≤ g

Tactic:
simp only [le_def', mk_lt, mk_eq]

Result:
f g : CauSeq ℚ abs
⊢ f < g ∨ f ≈ g ↔ f ≤ g
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem pmap_eq_attachWith {p q : α → Prop} (f : ∀ a, p a → q a) (l H) :
    pmap (fun a h => ⟨a, f a h⟩) l H = l.attachWith q (fun x h => f x (H x h))

Proof state:
case mk
α : Type u_1
p q : α → Prop
f : ∀ (a : α), p a → q a
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ pmap (fun a h => ⟨a, ⋯⟩) { toList := toList✝ } H = { toList := toList✝ }.attachWith q ⋯

Tactic:
simp [List.pmap_eq_attachWith]

Result:
no goals

Proof state:
α : Type u_1
p q : α → Prop
f : ∀ (a : α), p a → q a
l : Array α
H : ∀ (a : α), a ∈ l → p a
⊢ pmap (fun a h => ⟨a, ⋯⟩) l H = l.attachWith q ⋯

Tactic:
cases l

Result:
case mk
α : Type u_1
p q : α → Prop
f : ∀ (a : α), p a → q a
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ pmap (fun a h => ⟨a, ⋯⟩) { toList := toList✝ } H = { toList := toList✝ }.attachWith q ⋯
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_pos (n : ℕ) (s : S) (h : 0 < s) : 0 < (ascPochhammer S n).eval s

Proof state:
case succ
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (ascPochhammer S n)
⊢ 0 < eval s (ascPochhammer S (n + 1))

Tactic:
rw [ascPochhammer_succ_right, mul_add, eval_add, ← Nat.cast_comm, eval_natCast_mul, eval_mul_X,
  Nat.cast_comm, ← mul_add]

Result:
case succ
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (ascPochhammer S n)
⊢ 0 < eval s (ascPochhammer S n) * (s + ↑n)

Proof state:
S : Type u_1
inst✝ : StrictOrderedSemiring S
n : ℕ
s : S
h : 0 < s
⊢ 0 < eval s (ascPochhammer S n)

Tactic:
induction n with
| zero =>
  simp only [ascPochhammer_zero, eval_one]
  exact zero_lt_one
| succ n ih =>
  rw [ascPochhammer_succ_right, mul_add, eval_add, ← Nat.cast_comm, eval_natCast_mul, eval_mul_X,
    Nat.cast_comm, ← mul_add]
  exact mul_pos ih (lt_of_lt_of_le h (le_add_of_nonneg_right (Nat.cast_nonneg n)))

Result:
no goals

Proof state:
case succ
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (ascPochhammer S n)
⊢ 0 < eval s (ascPochhammer S n) * (s + ↑n)

Tactic:
exact mul_pos ih (lt_of_lt_of_le h (le_add_of_nonneg_right (Nat.cast_nonneg n)))

Result:
no goals

Proof state:
case zero
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
⊢ 0 < 1

Tactic:
exact zero_lt_one

Result:
no goals

Proof state:
case zero
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
⊢ 0 < eval s (ascPochhammer S 0)

Tactic:
simp only [ascPochhammer_zero, eval_one]

Result:
case zero
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
⊢ 0 < 1
-- Mathlib/Analysis/Normed/Module/WeakDual.lean
theorem dual_norm_topology_le_weak_dual_topology :
    (UniformSpace.toTopologicalSpace : TopologicalSpace (Dual 𝕜 E)) ≤
      (WeakDual.instTopologicalSpace : TopologicalSpace (WeakDual 𝕜 E))

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ UniformSpace.toTopologicalSpace ≤ WeakDual.instTopologicalSpace

Tactic:
convert (@toWeakDual_continuous _ _ _ _ (by assumption)).le_induced

Result:
case h.e'_4
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ WeakDual.instTopologicalSpace = TopologicalSpace.induced (fun x' => toWeakDual x') WeakDual.instTopologicalSpace

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ NormedSpace ?m.22271 ?m.22273

Tactic:
assumption

Result:
no goals

Proof state:
case h.e'_4
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ WeakDual.instTopologicalSpace = TopologicalSpace.induced (fun x' => toWeakDual x') WeakDual.instTopologicalSpace

Tactic:
exact induced_id.symm

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Basic.lean
@[simp]
lemma range_liftBaseChange (l : M →ₗ[R] N) :
    LinearMap.range (l.liftBaseChange A) = Submodule.span A (LinearMap.range l)

Proof state:
case a.intro.tmul
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x✝ : A
y✝ : M
⊢ (liftBaseChange A l) (x✝ ⊗ₜ[R] y✝) ∈ Submodule.span A ↑(range l)

Tactic:
rw [LinearMap.liftBaseChange_tmul]

Result:
case a.intro.tmul
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x✝ : A
y✝ : M
⊢ x✝ • l y✝ ∈ Submodule.span A ↑(range l)

Proof state:
case a.intro.zero
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
⊢ (liftBaseChange A l) 0 ∈ Submodule.span A ↑(range l)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x : M
⊢ (liftBaseChange A l) (1 ⊗ₜ[R] x) = l x

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
lemma map_variableChange (C : VariableChange R) :
    (W.map φ).variableChange (C.map φ) = (W.variableChange C).map φ

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C : VariableChange R
⊢ (W.map φ).variableChange (VariableChange.map φ C) = (W.variableChange C).map φ

Tactic:
simp only [map, variableChange, VariableChange.map]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C : VariableChange R
⊢ { a₁ := ↑((Units.map ↑φ) C.u)⁻¹ * (φ W.a₁ + 2 * φ C.s),
      a₂ := ↑((Units.map ↑φ) C.u)⁻¹ ^ 2 * (φ W.a₂ - φ C.s * φ W.a₁ + 3 * φ C.r - φ C.s ^ 2),
      a₃ := ↑((Units.map ↑φ) C.u)⁻¹ ^ 3 * (φ W.a₃ + φ C.r * φ W.a₁ + 2 * φ C.t),
      a₄ :=
        ↑((Units.map ↑φ) C.u)⁻¹ ^ 4 *
          (φ W.a₄ - φ C.s * φ W.a₃ + 2 * φ C.r * φ W.a₂ - (φ C.t + φ C.r * φ C.s) * φ W.a₁ + 3 * φ C.r ^ 2 -
            2 * φ C.s * φ C.t),
      a₆ :=
        ↑((Units.map ↑φ) C.u)⁻¹ ^ 6 *
          (φ W.a₆ + φ C.r * φ W.a₄ + φ C.r ^ 2 * φ W.a₂ + φ C.r ^ 3 - φ C.t * φ W.a₃ - φ C.t ^ 2 -
            φ C.r * φ C.t * φ W.a₁) } =
    { a₁ := φ (↑C.u⁻¹ * (W.a₁ + 2 * C.s)), a₂ := φ (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)),
      a₃ := φ (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)),
      a₄ :=
        φ (↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)),
      a₆ := φ (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) }

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C : VariableChange R
⊢ { a₁ := ↑((Units.map ↑φ) C.u)⁻¹ * (φ W.a₁ + 2 * φ C.s),
      a₂ := ↑((Units.map ↑φ) C.u)⁻¹ ^ 2 * (φ W.a₂ - φ C.s * φ W.a₁ + 3 * φ C.r - φ C.s ^ 2),
      a₃ := ↑((Units.map ↑φ) C.u)⁻¹ ^ 3 * (φ W.a₃ + φ C.r * φ W.a₁ + 2 * φ C.t),
      a₄ :=
        ↑((Units.map ↑φ) C.u)⁻¹ ^ 4 *
          (φ W.a₄ - φ C.s * φ W.a₃ + 2 * φ C.r * φ W.a₂ - (φ C.t + φ C.r * φ C.s) * φ W.a₁ + 3 * φ C.r ^ 2 -
            2 * φ C.s * φ C.t),
      a₆ :=
        ↑((Units.map ↑φ) C.u)⁻¹ ^ 6 *
          (φ W.a₆ + φ C.r * φ W.a₄ + φ C.r ^ 2 * φ W.a₂ + φ C.r ^ 3 - φ C.t * φ W.a₃ - φ C.t ^ 2 -
            φ C.r * φ C.t * φ W.a₁) } =
    { a₁ := φ (↑C.u⁻¹ * (W.a₁ + 2 * C.s)), a₂ := φ (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)),
      a₃ := φ (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)),
      a₄ :=
        φ (↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)),
      a₆ := φ (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) }

Tactic:
ext <;> map_simp <;> simp only [Units.coe_map, Units.coe_map_inv, MonoidHom.coe_coe]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma d_comp_ofHoms_v (ψ : ∀ (p : ℤ), F.X p ⟶ G.X p) (p' p q : ℤ) (hpq : p + 0 = q) :
    F.d p' p ≫ (ofHoms ψ).v p q hpq = F.d p' q ≫ ψ q

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p' p q : ℤ
hpq : p + 0 = q
⊢ F.d p' p ≫ (ofHoms ψ).v p q hpq = F.d p' q ≫ ψ q

Tactic:
rw [add_zero] at hpq

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p' p q : ℤ
hpq✝ : p + 0 = q
hpq : p = q
⊢ F.d p' p ≫ (ofHoms ψ).v p q hpq✝ = F.d p' q ≫ ψ q

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p' p q : ℤ
hpq✝ : p + 0 = q
hpq : p = q
⊢ F.d p' p ≫ (ofHoms ψ).v p q hpq✝ = F.d p' q ≫ ψ q

Tactic:
subst hpq

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p' p : ℤ
hpq : p + 0 = p
⊢ F.d p' p ≫ (ofHoms ψ).v p p hpq = F.d p' p ≫ ψ p

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p' p : ℤ
hpq : p + 0 = p
⊢ F.d p' p ≫ (ofHoms ψ).v p p hpq = F.d p' p ≫ ψ p

Tactic:
rw [ofHoms_v]

Result:
no goals