harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Fold.lean
theorem fold_op_rel_iff_and {r : β → β → Prop} (hr : ∀ {x y z}, r x (op y z) ↔ r x y ∧ r x z)
    {c : β} : r c (s.fold op b f) ↔ r c b ∧ ∀ x ∈ s, r c (f x)

Proof state:
case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
⊢ (r c (f a) ∧ ∀ x ∈ s, r c (f x)) ↔ ∀ x ∈ insert a s, r c (f x)

Tactic:
constructor

Result:
case insert.mp
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
⊢ (r c (f a) ∧ ∀ x ∈ s, r c (f x)) → ∀ x ∈ insert a s, r c (f x)

case insert.mpr
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
⊢ (∀ x ∈ insert a s, r c (f x)) → r c (f a) ∧ ∀ x ∈ s, r c (f x)

Proof state:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)

Tactic:
induction' s using Finset.induction_on with a s ha IH

Result:
case empty
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
⊢ r c (fold op b f ∅) ↔ r c b ∧ ∀ x ∈ ∅, r c (f x)

case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
⊢ r c (fold op b f (insert a s)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)
-- Mathlib/Analysis/Normed/Field/Lemmas.lean
@[simp]
protected lemma continuousAt_zpow : ContinuousAt (fun x ↦ x ^ n) x ↔ x ≠ 0 ∨ 0 ≤ n

Proof state:
𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
n : ℤ
x : 𝕜
⊢ ContinuousAt (fun x => x ^ n) x ↔ x ≠ 0 ∨ 0 ≤ n

Tactic:
refine ⟨?_, continuousAt_zpow₀ _ _⟩

Result:
𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
n : ℤ
x : 𝕜
⊢ ContinuousAt (fun x => x ^ n) x → x ≠ 0 ∨ 0 ≤ n

Proof state:
𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
n : ℤ
x : 𝕜
⊢ ContinuousAt (fun x => x ^ n) x → x ≠ 0 ∨ 0 ≤ n

Tactic:
contrapose!

Result:
𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
n : ℤ
x : 𝕜
⊢ x = 0 ∧ n < 0 → ¬ContinuousAt (fun x => x ^ n) x

Proof state:
case intro
𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
n : ℤ
hm : n < 0
hc : ContinuousAt (fun x => x ^ n) 0
⊢ False

Tactic:
exact not_tendsto_atTop_of_tendsto_nhds (hc.tendsto.mono_left nhdsWithin_le_nhds).norm
  (NormedField.tendsto_norm_zpow_nhdsNE_zero_atTop hm)

Result:
no goals

Proof state:
𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
n : ℤ
x : 𝕜
⊢ x = 0 ∧ n < 0 → ¬ContinuousAt (fun x => x ^ n) x

Tactic:
rintro ⟨rfl, hm⟩ hc

Result:
case intro
𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
n : ℤ
hm : n < 0
hc : ContinuousAt (fun x => x ^ n) 0
⊢ False
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem infinite_pigeonhole_card {β α : Type u} (f : β → α) (θ : Cardinal) (hθ : θ ≤ #β)
    (h₁ : ℵ₀ ≤ θ) (h₂ : #α < θ.ord.cof) : ∃ a : α, θ ≤ #(f ⁻¹' {a})

Proof state:
case intro.intro
β α : Type u
f : β → α
s : Set β
hθ : #↑s ≤ #β
h₁ : ℵ₀ ≤ #↑s
h₂ : #α < (#↑s).ord.cof
a : α
ha : #↑(f ∘ Subtype.val ⁻¹' {a}) = #↑s
⊢ ∃ a, #↑s ≤ #↑(f ⁻¹' {a})

Tactic:
use a

Result:
case h
β α : Type u
f : β → α
s : Set β
hθ : #↑s ≤ #β
h₁ : ℵ₀ ≤ #↑s
h₂ : #α < (#↑s).ord.cof
a : α
ha : #↑(f ∘ Subtype.val ⁻¹' {a}) = #↑s
⊢ #↑s ≤ #↑(f ⁻¹' {a})

Proof state:
case h
β α : Type u
f : β → α
s : Set β
hθ : #↑s ≤ #β
h₁ : ℵ₀ ≤ #↑s
h₂ : #α < (#↑s).ord.cof
a : α
ha : #↑(f ∘ Subtype.val ⁻¹' {a}) = #↑s
⊢ #↑(Subtype.val ⁻¹' (f ⁻¹' {a})) ≤ #↑(f ⁻¹' {a})

Tactic:
exact mk_preimage_of_injective _ _ Subtype.val_injective

Result:
no goals

Proof state:
β α : Type u
f : β → α
θ : Cardinal.{u}
hθ : θ ≤ #β
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
⊢ ∃ a, θ ≤ #↑(f ⁻¹' {a})

Tactic:
rcases le_mk_iff_exists_set.1 hθ with ⟨s, rfl⟩

Result:
case intro
β α : Type u
f : β → α
s : Set β
hθ : #↑s ≤ #β
h₁ : ℵ₀ ≤ #↑s
h₂ : #α < (#↑s).ord.cof
⊢ ∃ a, #↑s ≤ #↑(f ⁻¹' {a})

Proof state:
case h
β α : Type u
f : β → α
s : Set β
hθ : #↑s ≤ #β
h₁ : ℵ₀ ≤ #↑s
h₂ : #α < (#↑s).ord.cof
a : α
ha : #↑(f ∘ Subtype.val ⁻¹' {a}) = #↑s
⊢ #↑s ≤ #↑(f ⁻¹' {a})

Tactic:
rw [← ha, @preimage_comp _ _ _ Subtype.val f]

Result:
case h
β α : Type u
f : β → α
s : Set β
hθ : #↑s ≤ #β
h₁ : ℵ₀ ≤ #↑s
h₂ : #α < (#↑s).ord.cof
a : α
ha : #↑(f ∘ Subtype.val ⁻¹' {a}) = #↑s
⊢ #↑(Subtype.val ⁻¹' (f ⁻¹' {a})) ≤ #↑(f ⁻¹' {a})

Proof state:
case intro
β α : Type u
f : β → α
s : Set β
hθ : #↑s ≤ #β
h₁ : ℵ₀ ≤ #↑s
h₂ : #α < (#↑s).ord.cof
⊢ ∃ a, #↑s ≤ #↑(f ⁻¹' {a})

Tactic:
obtain ⟨a, ha⟩ := infinite_pigeonhole (f ∘ Subtype.val : s → α) h₁ h₂

Result:
case intro.intro
β α : Type u
f : β → α
s : Set β
hθ : #↑s ≤ #β
h₁ : ℵ₀ ≤ #↑s
h₂ : #α < (#↑s).ord.cof
a : α
ha : #↑(f ∘ Subtype.val ⁻¹' {a}) = #↑s
⊢ ∃ a, #↑s ≤ #↑(f ⁻¹' {a})
-- Mathlib/Analysis/SpecialFunctions/Stirling.lean
theorem second_wallis_limit (a : ℝ) (hane : a ≠ 0) (ha : Tendsto stirlingSeq atTop (𝓝 a)) :
    Tendsto Wallis.W atTop (𝓝 (a ^ 2 / 2))

Proof state:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
h : a ^ 2 / 2 = a ^ 4 / a ^ 2 * (1 / 2)
⊢ Tendsto (fun n => stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1))) atTop (𝓝 (a ^ 2 / 2))

Tactic:
rw [h]

Result:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
h : a ^ 2 / 2 = a ^ 4 / a ^ 2 * (1 / 2)
⊢ Tendsto (fun n => stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1))) atTop
    (𝓝 (a ^ 4 / a ^ 2 * (1 / 2)))

Proof state:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
h : a ^ 2 / 2 = a ^ 4 / a ^ 2 * (1 / 2)
⊢ Tendsto (fun n => stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1))) atTop
    (𝓝 (a ^ 4 / a ^ 2 * (1 / 2)))

Tactic:
exact ((ha.pow 4).div ((ha.comp (tendsto_id.const_mul_atTop' two_pos)).pow 2)
  (pow_ne_zero 2 hane)).mul tendsto_self_div_two_mul_self_add_one

Result:
no goals

Proof state:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ Tendsto Wallis.W atTop (𝓝 (a ^ 2 / 2))

Tactic:
refine Tendsto.congr' (eventually_atTop.mpr ⟨1, fun n hn =>
  stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq n (one_le_iff_ne_zero.mp hn)⟩) ?_

Result:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ Tendsto (fun n => stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1))) atTop (𝓝 (a ^ 2 / 2))

Proof state:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ Tendsto (fun n => stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1))) atTop (𝓝 (a ^ 2 / 2))

Tactic:
have h : a ^ 2 / 2 = a ^ 4 / a ^ 2 * (1 / 2) := by
  rw [mul_one_div, ← mul_one_div (a ^ 4) (a ^ 2), one_div, ← pow_sub_of_lt a]
  norm_num

Result:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
h : a ^ 2 / 2 = a ^ 4 / a ^ 2 * (1 / 2)
⊢ Tendsto (fun n => stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1))) atTop (𝓝 (a ^ 2 / 2))

Proof state:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ a ^ 2 / 2 = a ^ 4 / a ^ 2 * (1 / 2)

Tactic:
rw [mul_one_div, ← mul_one_div (a ^ 4) (a ^ 2), one_div, ← pow_sub_of_lt a]

Result:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ 2 < 4

Proof state:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ 2 < 4

Tactic:
norm_num

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem dvd_emod_sub_self {x : Int} {m : Nat} : (m : Int) ∣ x % m - x

Proof state:
case H
x : Int
m : Nat
⊢ (x % ↑m - x) % ↑m = 0

Tactic:
simp [sub_emod]

Result:
no goals

Proof state:
x : Int
m : Nat
⊢ ↑m ∣ x % ↑m - x

Tactic:
apply dvd_of_emod_eq_zero

Result:
case H
x : Int
m : Nat
⊢ (x % ↑m - x) % ↑m = 0
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_X_mul : (X * p).smeval x = x * p.smeval x

Proof state:
case h_monomial
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
a : R
⊢ (X * (monomial n) a).smeval x = x * ((monomial n) a).smeval x

Tactic:
rw [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, one_mul, npow_add,
  npow_one, ← mul_smul_comm, smeval_monomial]

Result:
no goals

Proof state:
case h_add
R : Type u_1
inst✝⁵ : Semiring R
p✝ : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
p q : R[X]
ph : (X * p).smeval x = x * p.smeval x
qh : (X * q).smeval x = x * q.smeval x
⊢ (X * (p + q)).smeval x = x * (p + q).smeval x

Tactic:
simp only [smeval_add, ph, qh, mul_add]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
⊢ (X * p).smeval x = x * p.smeval x

Tactic:
induction p using Polynomial.induction_on' with
| h_add p q ph qh =>
simp only [smeval_add, ph, qh, mul_add]
| h_monomial n a =>
rw [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, one_mul, npow_add,
  npow_one, ← mul_smul_comm, smeval_monomial]

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem forall_liouvilleWith_iff {x : ℝ} : (∀ p, LiouvilleWith p x) ↔ Liouville x

Proof state:
x : ℝ
⊢ (∀ (p : ℝ), LiouvilleWith p x) ↔ Liouville x

Tactic:
refine ⟨fun H n => ?_, Liouville.liouvilleWith⟩

Result:
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n : ℕ
⊢ ∃ a b, 1 < b ∧ x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n

Proof state:
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n : ℕ
⊢ ∃ a b, 1 < b ∧ x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n

Tactic:
rcases ((eventually_gt_atTop 1).and_frequently
  ((H (n + 1)).frequently_lt_rpow_neg (lt_add_one (n : ℝ)))).exists
  with ⟨b, hb, a, hne, hlt⟩

Result:
case intro.intro.intro.intro
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n b : ℕ
hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < ↑b ^ (-↑n)
⊢ ∃ a b, 1 < b ∧ x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n

Proof state:
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n b : ℕ
hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < ↑b ^ (-↑n)
⊢ |x - ↑a / ↑↑b| < 1 / ↑↑b ^ n

Tactic:
simpa [rpow_neg] using hlt

Result:
no goals

Proof state:
case intro.intro.intro.intro
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n b : ℕ
hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < ↑b ^ (-↑n)
⊢ ∃ a b, 1 < b ∧ x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n

Tactic:
exact ⟨a, b, mod_cast hb, hne, by simpa [rpow_neg] using hlt⟩

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem intValuation_zero_le (x : nonZeroDivisors R) : 0 < v.intValuationDef x

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : ↥(nonZeroDivisors R)
⊢ 0 < ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑x})).factors)))

Tactic:
exact WithZero.zero_lt_coe _

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : ↥(nonZeroDivisors R)
⊢ 0 < v.intValuationDef ↑x

Tactic:
rw [v.intValuationDef_if_neg (nonZeroDivisors.coe_ne_zero x)]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : ↥(nonZeroDivisors R)
⊢ 0 < ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑x})).factors)))
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem LinearMap.toMatrix₂_comp (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (f : M₁' →ₗ[R] M₁) :
    LinearMap.toMatrix₂ b₁' b₂ (B.comp f) =
      (toMatrix b₁' b₁ f)ᵀ * LinearMap.toMatrix₂ b₁ b₂ B

Proof state:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
n : Type u_11
m : Type u_12
n' : Type u_13
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁'
b₁' : Basis n' R M₁'
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₁' →ₗ[R] M₁
⊢ ((toMatrix b₁' b₁) f)ᵀ * (toMatrix₂ b₁ b₂) B * (toMatrix b₂ b₂) id = ((toMatrix b₁' b₁) f)ᵀ * (toMatrix₂ b₁ b₂) B

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
n : Type u_11
m : Type u_12
n' : Type u_13
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁'
b₁' : Basis n' R M₁'
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₁' →ₗ[R] M₁
⊢ (toMatrix₂ b₁' b₂) (B ∘ₗ f) = ((toMatrix b₁' b₁) f)ᵀ * (toMatrix₂ b₁ b₂) B

Tactic:
rw [← LinearMap.compl₂_id (B.comp f), ← LinearMap.compl₁₂, LinearMap.toMatrix₂_compl₁₂ b₁ b₂]

Result:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
n : Type u_11
m : Type u_12
n' : Type u_13
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁'
b₁' : Basis n' R M₁'
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₁' →ₗ[R] M₁
⊢ ((toMatrix b₁' b₁) f)ᵀ * (toMatrix₂ b₁ b₂) B * (toMatrix b₂ b₂) id = ((toMatrix b₁' b₁) f)ᵀ * (toMatrix₂ b₁ b₂) B
-- Mathlib/Data/Matrix/Notation.lean
theorem one_fin_two : (1 : Matrix (Fin 2) (Fin 2) α) = !![1, 0; 0, 1]

Proof state:
case a
α : Type u
inst✝¹ : Zero α
inst✝ : One α
i j : Fin 2
⊢ 1 i j = !![1, 0; 0, 1] i j

Tactic:
fin_cases i <;> fin_cases j <;> rfl

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 = !![1, 0; 0, 1]

Tactic:
ext i j

Result:
case a
α : Type u
inst✝¹ : Zero α
inst✝ : One α
i j : Fin 2
⊢ 1 i j = !![1, 0; 0, 1] i j
-- Mathlib/RingTheory/Generators.lean
lemma ker_eq_ker_aeval_val : P.ker = RingHom.ker (aeval P.val)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
⊢ RingHom.ker ↑(aeval P.val) = RingHom.ker (aeval P.val)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
⊢ P.ker = RingHom.ker (aeval P.val)

Tactic:
simp only [ker, Extension.ker, toExtension_Ring, algebraMap_eq]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
⊢ RingHom.ker ↑(aeval P.val) = RingHom.ker (aeval P.val)
-- Mathlib/Algebra/Order/Star/Basic.lean
theorem mul_star_self_pos [Nontrivial R] {x : R} (hx : IsRegular x) : 0 < x * star x

Proof state:
R : Type u
inst✝⁴ : NonUnitalSemiring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : Nontrivial R
x : R
hx : IsRegular x
⊢ 0 < x * star x

Tactic:
simpa using star_mul_self_pos hx.star

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_of_mem_push_of_mem {a b : α} {l : Array α} : a ∈ l.push b → b ∈ l → a ∈ l

Proof state:
case mk.inl
α : Type u_1
a b : α
toList✝ : List α
h : a ∈ toList✝
a✝ : b ∈ toList✝
⊢ a ∈ toList✝

Tactic:
exact h

Result:
no goals

Proof state:
case mk
α : Type u_1
a b : α
toList✝ : List α
⊢ a ∈ toList✝ ∨ a = b → b ∈ toList✝ → a ∈ toList✝

Tactic:
rintro (h | rfl)

Result:
case mk.inl
α : Type u_1
a b : α
toList✝ : List α
h : a ∈ toList✝
⊢ b ∈ toList✝ → a ∈ toList✝

case mk.inr
α : Type u_1
a : α
toList✝ : List α
⊢ a ∈ toList✝ → a ∈ toList✝

Proof state:
case mk.inl
α : Type u_1
a b : α
toList✝ : List α
h : a ∈ toList✝
⊢ b ∈ toList✝ → a ∈ toList✝

Tactic:
intro _

Result:
case mk.inl
α : Type u_1
a b : α
toList✝ : List α
h : a ∈ toList✝
a✝ : b ∈ toList✝
⊢ a ∈ toList✝

Proof state:
α : Type u_1
a b : α
l : Array α
⊢ a ∈ l.push b → b ∈ l → a ∈ l

Tactic:
cases l

Result:
case mk
α : Type u_1
a b : α
toList✝ : List α
⊢ a ∈ { toList := toList✝ }.push b → b ∈ { toList := toList✝ } → a ∈ { toList := toList✝ }

Proof state:
case mk
α : Type u_1
a b : α
toList✝ : List α
⊢ a ∈ { toList := toList✝ }.push b → b ∈ { toList := toList✝ } → a ∈ { toList := toList✝ }

Tactic:
simp only [List.push_toArray, mem_toArray, List.mem_append, List.mem_singleton]

Result:
case mk
α : Type u_1
a b : α
toList✝ : List α
⊢ a ∈ toList✝ ∨ a = b → b ∈ toList✝ → a ∈ toList✝

Proof state:
case mk.inr
α : Type u_1
a : α
toList✝ : List α
⊢ a ∈ toList✝ → a ∈ toList✝

Tactic:
exact id

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
@[simp]
lemma map_dblU {K : Type v} [Field K] (f : F →+* K) (P : Fin 3 → F) :
    (W.map f).toProjective.dblU (f ∘ P) = f (W.dblU P)

Proof state:
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P : Fin 3 → F
⊢ ((map W f).toProjective.a₁ * (⇑f ∘ P) y * (⇑f ∘ P) z -
          (3 * (⇑f ∘ P) x ^ 2 + 2 * (map W f).toProjective.a₂ * (⇑f ∘ P) x * (⇑f ∘ P) z +
            (map W f).toProjective.a₄ * (⇑f ∘ P) z ^ 2)) ^
        3 /
      (⇑f ∘ P) z ^ 2 =
    f ((W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z + W.a₄ * P z ^ 2)) ^ 3 / P z ^ 2)

Tactic:
map_simp

Result:
no goals

Proof state:
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P : Fin 3 → F
⊢ (map W f).toProjective.dblU (⇑f ∘ P) = f (W.dblU P)

Tactic:
simp only [dblU_eq]

Result:
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P : Fin 3 → F
⊢ ((map W f).toProjective.a₁ * (⇑f ∘ P) y * (⇑f ∘ P) z -
          (3 * (⇑f ∘ P) x ^ 2 + 2 * (map W f).toProjective.a₂ * (⇑f ∘ P) x * (⇑f ∘ P) z +
            (map W f).toProjective.a₄ * (⇑f ∘ P) z ^ 2)) ^
        3 /
      (⇑f ∘ P) z ^ 2 =
    f ((W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z + W.a₄ * P z ^ 2)) ^ 3 / P z ^ 2)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem lt_irrefl (a : Int) : ¬a < a := fun H =>
  let ⟨n, hn⟩ := lt.dest H
  have : (a+Nat.succ n) = a+0

Proof state:
a : Int
H : a < a
n : Nat
hn : a + ↑n.succ = a
⊢ a + ↑n.succ = a + 0

Tactic:
rw [hn, Int.add_zero]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem head_some_of_get?_some {s : WSeq α} {a n} (h : some a ∈ get? s n) :
    ∃ a', some a' ∈ head s

Proof state:
case succ
α : Type u
s : WSeq α
n : ℕ
IH : ∀ {a : α}, some a ∈ s.get? n → ∃ a', some a' ∈ s.head
a : α
h : some a ∈ s.get? (n + 1)
a' : α
h' : some a' ∈ (s.drop n).head
⊢ ∃ a', some a' ∈ s.head

Tactic:
exact IH h'

Result:
no goals

Proof state:
α : Type u
s : WSeq α
a : α
n : ℕ
h : some a ∈ s.get? n
⊢ ∃ a', some a' ∈ s.head

Tactic:
induction n generalizing a with
| zero => exact ⟨_, h⟩
| succ n IH =>
    let ⟨a', h'⟩ := head_some_of_head_tail_some h
    exact IH h'

Result:
no goals

Proof state:
case zero
α : Type u
s : WSeq α
a : α
h : some a ∈ s.get? 0
⊢ ∃ a', some a' ∈ s.head

Tactic:
exact ⟨_, h⟩

Result:
no goals

Proof state:
case succ
α : Type u
s : WSeq α
n : ℕ
IH : ∀ {a : α}, some a ∈ s.get? n → ∃ a', some a' ∈ s.head
a : α
h : some a ∈ s.get? (n + 1)
⊢ ∃ a', some a' ∈ s.head

Tactic:
let ⟨a', h'⟩ := head_some_of_head_tail_some h

Result:
case succ
α : Type u
s : WSeq α
n : ℕ
IH : ∀ {a : α}, some a ∈ s.get? n → ∃ a', some a' ∈ s.head
a : α
h : some a ∈ s.get? (n + 1)
a' : α
h' : some a' ∈ (s.drop n).head
⊢ ∃ a', some a' ∈ s.head
-- Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean
theorem isPurelyInseparable_iff_perfectClosure_eq_top :
    IsPurelyInseparable F E ↔ perfectClosure F E = ⊤

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsPurelyInseparable F E ↔ perfectClosure F E = ⊤

Tactic:
rw [isPurelyInseparable_iff_pow_mem F (ringExpChar F)]

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ (∀ (x : E), ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F E).range) ↔ perfectClosure F E = ⊤

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ (∀ (x : E), ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F E).range) ↔ perfectClosure F E = ⊤

Tactic:
exact ⟨fun H ↦ top_unique fun x _ ↦ H x, fun H _ ↦ H.ge trivial⟩

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem tendsto_of_uniformContinuous_subtype [UniformSpace α] [UniformSpace β] {f : α → β}
    {s : Set α} {a : α} (hf : UniformContinuous fun x : s => f x.val) (ha : s ∈ 𝓝 a) :
    Tendsto f (𝓝 a) (𝓝 (f a))

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
a : α
hf : UniformContinuous fun x => f ↑x
ha : s ∈ 𝓝 a
⊢ Tendsto f (𝓝 a) (𝓝 (f a))

Tactic:
rw [(@map_nhds_subtype_coe_eq_nhds α _ s a (mem_of_mem_nhds ha) ha).symm]

Result:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
a : α
hf : UniformContinuous fun x => f ↑x
ha : s ∈ 𝓝 a
⊢ Tendsto f (map Subtype.val (𝓝 ⟨a, ⋯⟩)) (𝓝 (f a))

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
a : α
hf : UniformContinuous fun x => f ↑x
ha : s ∈ 𝓝 a
⊢ Tendsto f (map Subtype.val (𝓝 ⟨a, ⋯⟩)) (𝓝 (f a))

Tactic:
exact tendsto_map' hf.continuous.continuousAt

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma nonsingular_add {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) :
    W.Nonsingular <| W.add P Q

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
⊢ W.Nonsingular (W.add P Q)

Tactic:
by_cases hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z

Result:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
⊢ W.Nonsingular (W.add P Q)

case neg
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ W.Nonsingular (W.add P Q)

Proof state:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
hy : P y * Q z = Q y * P z
⊢ W.Nonsingular (W.add P Q)

Tactic:
simp only [add_of_Y_eq hP.left hPz hQz hxy.left hy hxy.right, nonsingular_smul _ <|
    isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, nonsingular_zero]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
⊢ W.Nonsingular (W.add P Q)

Tactic:
by_cases hPz : P z = 0

Result:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
⊢ W.Nonsingular (W.add P Q)

case neg
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
⊢ W.Nonsingular (W.add P Q)