harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Dimension/ErdosKaplansky.lean
theorem rank_dual_eq_card_dual_of_aleph0_le_rank {K V} [Field K] [AddCommGroup V] [Module K V]
    (h : ℵ₀ ≤ Module.rank K V) : Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)

Proof state:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := K) (M := V)

Result:
case intro.mk
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type u_2
b : Basis ι K V
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)

Proof state:
case intro.mk
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_2
h : Infinite ι
b : Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[K] ι → K
⊢ Module.rank K (ι → K) = #(ι → K)

Tactic:
apply rank_fun_infinite

Result:
no goals

Proof state:
case intro.mk
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type u_2
b : Basis ι K V
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
rw [← b.mk_eq_rank'', aleph0_le_mk_iff] at h

Result:
case intro.mk
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_2
h : Infinite ι
b : Basis ι K V
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)

Proof state:
case intro.mk
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_2
h : Infinite ι
b : Basis ι K V
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
have e := (b.constr K (M' := K)).symm

Result:
case intro.mk
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_2
h : Infinite ι
b : Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[K] ι → K
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)

Proof state:
case intro.mk
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_2
h : Infinite ι
b : Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[K] ι → K
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
rw [e.rank_eq, e.toEquiv.cardinal_eq]

Result:
case intro.mk
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_2
h : Infinite ι
b : Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[K] ι → K
⊢ Module.rank K (ι → K) = #(ι → K)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma twoTorsionPolynomial_disc_of_char_two : W.twoTorsionPolynomial.disc = 0

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.twoTorsionPolynomial.disc = 0

Tactic:
linear_combination W.twoTorsionPolynomial_disc + 8 * W.Δ * CharP.cast_eq_zero R 2

Result:
no goals
-- Mathlib/ModelTheory/Basic.lean
theorem symm_comp_self (f : M ≃[L] N) : f.symm.comp f = refl L M

Proof state:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
x✝ : M
⊢ (f.symm.comp f) x✝ = (refl L M) x✝

Tactic:
rw [comp_apply, symm_apply_apply, refl_apply]

Result:
no goals

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ f.symm.comp f = refl L M

Tactic:
ext

Result:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
x✝ : M
⊢ (f.symm.comp f) x✝ = (refl L M) x✝
-- Mathlib/Data/Set/Pointwise/SMul.lean
@[to_additive (attr := simp)]
lemma inv_smul_set_distrib (a : α) (s : Set α) : (a • s)⁻¹ = op a⁻¹ • s⁻¹

Proof state:
case h
α : Type u_2
inst✝ : Group α
a : α
s : Set α
x✝ : α
⊢ x✝ ∈ (a • s)⁻¹ ↔ x✝ ∈ op a⁻¹ • s⁻¹

Tactic:
simp [mem_smul_set_iff_inv_smul_mem]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Group α
a : α
s : Set α
⊢ (a • s)⁻¹ = op a⁻¹ • s⁻¹

Tactic:
ext

Result:
case h
α : Type u_2
inst✝ : Group α
a : α
s : Set α
x✝ : α
⊢ x✝ ∈ (a • s)⁻¹ ↔ x✝ ∈ op a⁻¹ • s⁻¹
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem eq_one_of_mul_right (h : a * b = 1) : a = 1 :=
  congr_arg Units.inv <| Subsingleton.elim (Units.mk _ _ (by rwa [mul_comm]) h) 1

Proof state:
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * a = 1

Tactic:
rwa [mul_comm]

Result:
no goals
-- Mathlib/Data/Vector/Snoc.lean
theorem reverse_cons : reverse (x ::ᵥ xs) = (reverse xs).snoc x

Proof state:
α : Type u_1
n : ℕ
x : α
xs : Vector α n
⊢ (x ::ᵥ xs).reverse = xs.reverse.snoc x

Tactic:
cases xs

Result:
case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : val✝.length = n
⊢ (x ::ᵥ ⟨val✝, property✝⟩).reverse = (reverse ⟨val✝, property✝⟩).snoc x

Proof state:
case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : val✝.length = n
⊢ (x ::ᵥ ⟨val✝, property✝⟩).reverse = (reverse ⟨val✝, property✝⟩).snoc x

Tactic:
simp only [reverse, cons, toList_mk, List.reverse_cons, snoc]

Result:
case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : val✝.length = n
⊢ ⟨val✝.reverse ++ [x], ⋯⟩ = append ⟨val✝.reverse, ⋯⟩ ⟨[x], ⋯⟩

Proof state:
case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : val✝.length = n
⊢ ⟨val✝.reverse ++ [x], ⋯⟩ = append ⟨val✝.reverse, ⋯⟩ ⟨[x], ⋯⟩

Tactic:
congr

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
theorem mul_pdf_integrable (hcs : IsCompact s) (huX : IsUniform X s ℙ) :
    Integrable fun x : ℝ => x * (pdf X ℙ volume x).toReal

Proof state:
case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ⊤
this : IsProbabilityMeasure ℙ
⊢ Integrable (fun x => x * (pdf X ℙ volume x).toReal) volume

Tactic:
constructor

Result:
case neg.left
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ⊤
this : IsProbabilityMeasure ℙ
⊢ AEStronglyMeasurable (fun x => x * (pdf X ℙ volume x).toReal) volume

case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ⊤
this : IsProbabilityMeasure ℙ
⊢ HasFiniteIntegral (fun x => x * (pdf X ℙ volume x).toReal) volume

Proof state:
case pos
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : volume s = 0 ∨ volume s = ⊤
I : Integrable (fun x => x * ENNReal.toReal 0) volume
⊢ (fun x => x * ENNReal.toReal 0) =ᶠ[ae volume] fun x => x * (pdf X ℙ volume x).toReal

Tactic:
filter_upwards [pdf_eq_zero_of_measure_eq_zero_or_top huX hnt] with x hx

Result:
case h
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : volume s = 0 ∨ volume s = ⊤
I : Integrable (fun x => x * ENNReal.toReal 0) volume
x : ℝ
hx : pdf X ℙ volume x = 0 x
⊢ x * ENNReal.toReal 0 = x * (pdf X ℙ volume x).toReal

Proof state:
case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ⊤
⊢ Integrable (fun x => x * (pdf X ℙ volume x).toReal) volume

Tactic:
have : IsProbabilityMeasure ℙ := isProbabilityMeasure hnt.1 hnt.2 huX

Result:
case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ⊤
this : IsProbabilityMeasure ℙ
⊢ Integrable (fun x => x * (pdf X ℙ volume x).toReal) volume
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem of_epi {X Y : C} (f : X ⟶ Y) [Epi f] (i : IsZero X) : IsZero Y

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
i : IsZero X
hf : f = 0
⊢ IsZero Y

Tactic:
subst hf

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
i : IsZero X
inst✝ : Epi 0
⊢ IsZero Y

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
i : IsZero X
inst✝ : Epi 0
⊢ IsZero Y

Tactic:
exact IsZero.of_epi_zero X Y

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
i : IsZero X
⊢ IsZero Y

Tactic:
have hf := i.eq_zero_of_src f

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
i : IsZero X
hf : f = 0
⊢ IsZero Y
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem not_isField : ¬IsField A⟦X⟧

Proof state:
case h.right
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ¬1 = 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
case h
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ⊥ < Ideal.span {X} ∧ Ideal.span {X} < ⊤

Tactic:
constructor

Result:
case h.left
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ⊥ < Ideal.span {X}

case h.right
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ Ideal.span {X} < ⊤

Proof state:
case h.left
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ¬X = 0

Tactic:
exact X_ne_zero

Result:
no goals

Proof state:
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ¬IsField A⟦X⟧

Tactic:
rw [Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top]

Result:
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ∃ I, ⊥ < I ∧ I < ⊤

Proof state:
case h.left
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ⊥ < Ideal.span {X}

Tactic:
rw [bot_lt_iff_ne_bot, Ne, Ideal.span_singleton_eq_bot]

Result:
case h.left
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ¬X = 0

Proof state:
case h.right
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ Ideal.span {X} < ⊤

Tactic:
rw [lt_top_iff_ne_top, Ne, Ideal.eq_top_iff_one, Ideal.mem_span_singleton,
  X_dvd_iff, constantCoeff_one]

Result:
case h.right
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ¬1 = 0

Proof state:
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ∃ I, ⊥ < I ∧ I < ⊤

Tactic:
use Ideal.span {X}

Result:
case h
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ⊥ < Ideal.span {X} ∧ Ideal.span {X} < ⊤

Proof state:
case pos
A : Type u_2
inst✝ : CommRing A
hA : Subsingleton A
⊢ ¬IsField A⟦X⟧

Tactic:
exact not_isField_of_subsingleton _

Result:
no goals

Proof state:
case neg
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
⊢ ¬IsField A⟦X⟧

Tactic:
nontriviality A

Result:
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ¬IsField A⟦X⟧

Proof state:
A : Type u_2
inst✝ : CommRing A
⊢ ¬IsField A⟦X⟧

Tactic:
by_cases hA : Subsingleton A

Result:
case pos
A : Type u_2
inst✝ : CommRing A
hA : Subsingleton A
⊢ ¬IsField A⟦X⟧

case neg
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
⊢ ¬IsField A⟦X⟧
-- Mathlib/Data/Int/Cast/Lemmas.lean
lemma _root_.zsmul_eq_mul' (a : α) (n : ℤ) : n • a = a * n

Proof state:
α : Type u_3
inst✝ : NonAssocRing α
a : α
n : ℤ
⊢ n • a = a * ↑n

Tactic:
rw [zsmul_eq_mul, (n.cast_commute a).eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem eraseIdx_eq_eraseIdxIfInBounds {a : Array α} {i : Nat} (h : i < a.size) :
    a.eraseIdx i h = a.eraseIdxIfInBounds i

Proof state:
α : Type u_1
a : Array α
i : Nat
h : i < a.size
⊢ a.eraseIdx i h = a.eraseIdxIfInBounds i

Tactic:
simp [eraseIdxIfInBounds, h]

Result:
no goals
-- Mathlib/Computability/Tape.lean
theorem ListBlank.head_map {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ')
    (l : ListBlank Γ) : (l.map f).head = f l.head

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ (map f l).head = f.f l.head

Tactic:
conv => lhs; rw [← ListBlank.cons_head_tail l]

Result:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ (map f (cons l.head l.tail)).head = f.f l.head

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ (map f (cons l.head l.tail)).head = f.f l.head

Tactic:
exact Quotient.inductionOn' l fun a ↦ rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem exists_nnnorm_eq_spectralRadius_of_nonempty [ProperSpace 𝕜] {a : A} (ha : (σ a).Nonempty) :
    ∃ k ∈ σ a, (‖k‖₊ : ℝ≥0∞) = spectralRadius 𝕜 a

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
a : A
ha : (σ a).Nonempty
⊢ ∃ k ∈ σ a, ↑‖k‖₊ = spectralRadius 𝕜 a

Tactic:
obtain ⟨k, hk, h⟩ := (spectrum.isCompact a).exists_isMaxOn ha continuous_nnnorm.continuousOn

Result:
case intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
a : A
ha : (σ a).Nonempty
k : 𝕜
hk : k ∈ σ a
h : IsMaxOn (fun a => ‖a‖₊) (σ a) k
⊢ ∃ k ∈ σ a, ↑‖k‖₊ = spectralRadius 𝕜 a

Proof state:
case intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
a : A
ha : (σ a).Nonempty
k : 𝕜
hk : k ∈ σ a
h : IsMaxOn (fun a => ‖a‖₊) (σ a) k
⊢ ∃ k ∈ σ a, ↑‖k‖₊ = spectralRadius 𝕜 a

Tactic:
exact ⟨k, hk, le_antisymm (le_iSup₂ (α := ℝ≥0∞) k hk) (iSup₂_le <| mod_cast h)⟩

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem mul_assoc' [NonUnitalSemiring R] (x y z : HahnSeries Γ R) :
    x * y * z = x * (y * z)

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ ∑ x_1 ∈ (addAntidiagonal ⋯ ⋯ b).sigma fun a => addAntidiagonal ⋯ ⋯ a.1,
      x.coeff x_1.snd.1 * y.coeff x_1.snd.2 * z.coeff x_1.fst.2 =
    ∑ x_1 ∈ (addAntidiagonal ⋯ ⋯ b).sigma fun a => addAntidiagonal ⋯ ⋯ a.2,
      x.coeff x_1.fst.1 * (y.coeff x_1.snd.1 * z.coeff x_1.snd.2)

Tactic:
apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l + j), (l, j)⟩)
  (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩) <;>
  aesop (add safe Set.add_mem_add) (add simp [add_assoc, mul_assoc])

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
⊢ x * y * z = x * (y * z)

Tactic:
ext b

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ (x * y * z).coeff b = (x * (y * z)).coeff b

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ ∑ ij ∈ addAntidiagonal ⋯ ⋯ b, (x * y).coeff ij.1 * z.coeff ij.2 =
    ∑ ij ∈ addAntidiagonal ⋯ ⋯ b, x.coeff ij.1 * (y * z).coeff ij.2

Tactic:
simp only [coeff_mul, coeff_add, sum_mul, mul_sum, sum_sigma']

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ ∑ x_1 ∈ (addAntidiagonal ⋯ ⋯ b).sigma fun a => addAntidiagonal ⋯ ⋯ a.1,
      x.coeff x_1.snd.1 * y.coeff x_1.snd.2 * z.coeff x_1.fst.2 =
    ∑ x_1 ∈ (addAntidiagonal ⋯ ⋯ b).sigma fun a => addAntidiagonal ⋯ ⋯ a.2,
      x.coeff x_1.fst.1 * (y.coeff x_1.snd.1 * z.coeff x_1.snd.2)

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ (x * y * z).coeff b = (x * (y * z)).coeff b

Tactic:
rw [coeff_mul_left' (x.isPWO_support.add y.isPWO_support) support_mul_subset_add_support,
  coeff_mul_right' (y.isPWO_support.add z.isPWO_support) support_mul_subset_add_support]

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ ∑ ij ∈ addAntidiagonal ⋯ ⋯ b, (x * y).coeff ij.1 * z.coeff ij.2 =
    ∑ ij ∈ addAntidiagonal ⋯ ⋯ b, x.coeff ij.1 * (y * z).coeff ij.2
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mpullbackWithin_neg :
    mpullbackWithin I I' f (-V) s = - mpullbackWithin I I' f V s

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
V : (x : M') → TangentSpace I' x
⊢ mpullbackWithin I I' f (-V) s = -mpullbackWithin I I' f V s

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
V : (x : M') → TangentSpace I' x
x : M
⊢ mpullbackWithin I I' f (-V) s x = (-mpullbackWithin I I' f V s) x

Proof state:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
V : (x : M') → TangentSpace I' x
x : M
⊢ mpullbackWithin I I' f (-V) s x = (-mpullbackWithin I I' f V s) x

Tactic:
simp [mpullbackWithin_apply]

Result:
no goals
-- Mathlib/SetTheory/Game/Domineering.lean
theorem snd_pred_mem_erase_of_mem_left {b : Board} {m : ℤ × ℤ} (h : m ∈ left b) :
    (m.1, m.2 - 1) ∈ b.erase m

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ b ∧ (m.1, m.2 - 1) ∈ b
⊢ (m.1, m.2 - 1) ∈ Finset.erase b m

Tactic:
apply Finset.mem_erase_of_ne_of_mem _ h.2

Result:
b : Board
m : ℤ × ℤ
h : m ∈ b ∧ (m.1, m.2 - 1) ∈ b
⊢ (m.1, m.2 - 1) ≠ m

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ (m.1, m.2 - 1) ∈ Finset.erase b m

Tactic:
rw [mem_left] at h

Result:
b : Board
m : ℤ × ℤ
h : m ∈ b ∧ (m.1, m.2 - 1) ∈ b
⊢ (m.1, m.2 - 1) ∈ Finset.erase b m

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ b ∧ (m.1, m.2 - 1) ∈ b
⊢ (m.1, m.2 - 1) ≠ m

Tactic:
exact ne_of_apply_ne Prod.snd (pred_ne_self m.2)

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_σ_succ' {n} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.succ) :
    X.δ j ≫ X.σ i = 𝟙 _

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.succ
⊢ X.δ j ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Tactic:
subst H

Result:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.δ i.succ ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.δ i.succ ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Tactic:
rw [δ_comp_σ_succ]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma add_of_Z_eq_zero_right {P Q : Fin 3 → R} (hQ : W'.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z = 0) : W'.add P Q = -(Q x * P z) • P

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z = 0
⊢ W'.add P Q = -(Q x * P z) • P

Tactic:
rw [add, if_neg <| not_equiv_of_Z_eq_zero_right hPz hQz, addXYZ_of_Z_eq_zero_right hQ hQz]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Circulant.lean
theorem pathGraph_le_cycleGraph {n : ℕ} : pathGraph n ≤ cycleGraph n

Proof state:
case inr
n✝ n : ℕ
u v : Fin (n + 2)
h : ↑v + 1 = ↑u
⊢ ↑(u - v) = 1 ∨ ↑(v - u) = 1

Tactic:
simp [Fin.coe_sub_iff_le.mpr (Nat.lt_of_succ_le h.le).le, Nat.eq_sub_of_add_eq' h]

Result:
no goals

Proof state:
n : ℕ
⊢ pathGraph n ≤ cycleGraph n

Tactic:
match n with
| 0 | 1 => simp
| n + 2 =>
  intro u v h
  rw [pathGraph_adj] at h
  rw [cycleGraph_adj']
  cases h with
  | inl h | inr h =>
    simp [Fin.coe_sub_iff_le.mpr (Nat.lt_of_succ_le h.le).le, Nat.eq_sub_of_add_eq' h]

Result:
no goals

Proof state:
n✝ n : ℕ
u v : Fin (n + 2)
h : (pathGraph (n + 2)).Adj u v
⊢ (cycleGraph (n + 2)).Adj u v

Tactic:
rw [pathGraph_adj] at h

Result:
n✝ n : ℕ
u v : Fin (n + 2)
h : ↑u + 1 = ↑v ∨ ↑v + 1 = ↑u
⊢ (cycleGraph (n + 2)).Adj u v

Proof state:
n : ℕ
⊢ pathGraph 1 ≤ cycleGraph 1

Tactic:
simp

Result:
no goals

Proof state:
n✝ n : ℕ
u v : Fin (n + 2)
h : ↑u + 1 = ↑v ∨ ↑v + 1 = ↑u
⊢ ↑(u - v) = 1 ∨ ↑(v - u) = 1

Tactic:
cases h with
| inl h | inr h =>
  simp [Fin.coe_sub_iff_le.mpr (Nat.lt_of_succ_le h.le).le, Nat.eq_sub_of_add_eq' h]

Result:
no goals

Proof state:
n✝ n : ℕ
u v : Fin (n + 2)
h : ↑u + 1 = ↑v ∨ ↑v + 1 = ↑u
⊢ (cycleGraph (n + 2)).Adj u v

Tactic:
rw [cycleGraph_adj']

Result:
n✝ n : ℕ
u v : Fin (n + 2)
h : ↑u + 1 = ↑v ∨ ↑v + 1 = ↑u
⊢ ↑(u - v) = 1 ∨ ↑(v - u) = 1

Proof state:
n✝ n : ℕ
⊢ pathGraph (n + 2) ≤ cycleGraph (n + 2)

Tactic:
intro u v h

Result:
n✝ n : ℕ
u v : Fin (n + 2)
h : (pathGraph (n + 2)).Adj u v
⊢ (cycleGraph (n + 2)).Adj u v
-- Mathlib/Condensed/Light/Epi.lean
lemma isLocallySurjective_iff_locallySurjective_on_lightProfinite : IsLocallySurjective f ↔
    ∀ (S : LightProfinite) (y : ToType (Y.val.obj ⟨S⟩)),
      (∃ (S' : LightProfinite) (φ : S' ⟶ S) (_ : Function.Surjective φ)
        (x : ToType (X.val.obj ⟨S'⟩)),
        f.val.app ⟨S'⟩ x = Y.val.map ⟨φ⟩ y)

Proof state:
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
X Y : LightCondensed A
f : X ⟶ Y
⊢ IsLocallySurjective f ↔
    ∀ (S : LightProfinite) (y : ToType (Y.val.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x,
            (ConcreteCategory.hom (f.val.app (Opposite.op S'))) x = (ConcreteCategory.hom (Y.val.map (Opposite.op φ))) y

Tactic:
rw [coherentTopology.isLocallySurjective_iff,
  regularTopology.isLocallySurjective_iff]

Result:
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
X Y : LightCondensed A
f : X ⟶ Y
⊢ (∀ (X_1 : LightProfinite) (y : ToType (Y.val.obj (Opposite.op X_1))),
      ∃ X' φ,
        ∃ (_ : EffectiveEpi φ),
          ∃ x,
            (ConcreteCategory.hom (f.val.app (Opposite.op X'))) x =
              (ConcreteCategory.hom (Y.val.map (Opposite.op φ))) y) ↔
    ∀ (S : LightProfinite) (y : ToType (Y.val.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x,
            (ConcreteCategory.hom (f.val.app (Opposite.op S'))) x = (ConcreteCategory.hom (Y.val.map (Opposite.op φ))) y

Proof state:
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
X Y : LightCondensed A
f : X ⟶ Y
⊢ (∀ (X_1 : LightProfinite) (y : ToType (Y.val.obj (Opposite.op X_1))),
      ∃ X' φ,
        ∃ (_ : EffectiveEpi φ),
          ∃ x,
            (ConcreteCategory.hom (f.val.app (Opposite.op X'))) x =
              (ConcreteCategory.hom (Y.val.map (Opposite.op φ))) y) ↔
    ∀ (S : LightProfinite) (y : ToType (Y.val.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x,
            (ConcreteCategory.hom (f.val.app (Opposite.op S'))) x = (ConcreteCategory.hom (Y.val.map (Opposite.op φ))) y

Tactic:
simp_rw [LightProfinite.effectiveEpi_iff_surjective]

Result:
no goals