harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem add_compLinearMap (f₁ f₂ : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) :
    (f₁ + f₂).compLinearMap g = f₁.compLinearMap g + f₂.compLinearMap g

Proof state:
case H
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_7
M₂ : Type u_10
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f₁ f₂ : M [⋀^ι]→ₗ[R] N
g : M₂ →ₗ[R] M
x✝ : ι → M₂
⊢ ((f₁ + f₂).compLinearMap g) x✝ = (f₁.compLinearMap g + f₂.compLinearMap g) x✝

Tactic:
simp only [compLinearMap_apply, add_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_7
M₂ : Type u_10
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f₁ f₂ : M [⋀^ι]→ₗ[R] N
g : M₂ →ₗ[R] M
⊢ (f₁ + f₂).compLinearMap g = f₁.compLinearMap g + f₂.compLinearMap g

Tactic:
ext

Result:
case H
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_7
M₂ : Type u_10
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f₁ f₂ : M [⋀^ι]→ₗ[R] N
g : M₂ →ₗ[R] M
x✝ : ι → M₂
⊢ ((f₁ + f₂).compLinearMap g) x✝ = (f₁.compLinearMap g + f₂.compLinearMap g) x✝
-- Mathlib/SetTheory/Cardinal/ENat.lean
lemma toENat_le_iff_of_le_aleph0 {c c' : Cardinal} (h : c ≤ ℵ₀) :
    toENat c ≤ toENat c' ↔ c ≤ c'

Proof state:
case intro
c' : Cardinal.{u_1}
c : ℕ∞
⊢ toENat ↑c ≤ toENat c' ↔ ↑c ≤ c'

Tactic:
simp_rw [toENat_ofENat, enat_gc _]

Result:
no goals

Proof state:
c c' : Cardinal.{u_1}
h : c ≤ ℵ₀
⊢ toENat c ≤ toENat c' ↔ c ≤ c'

Tactic:
lift c to ℕ∞ using h

Result:
case intro
c' : Cardinal.{u_1}
c : ℕ∞
⊢ toENat ↑c ≤ toENat c' ↔ ↑c ≤ c'
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[reassoc (attr := simp)]
lemma δ_natural_right {X Y : C} (X' : C) (f : X ⟶ Y) :
    δ F X' X ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ δ F X' Y

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y X' : C
f : X ⟶ Y
⊢ δ F X' X ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ δ F X' Y

Tactic:
apply δ'_natural_right

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lsub_eq_zero_iff {ι : Type u} (f : ι → Ordinal.{max u v}) :
    lsub.{_, v} f = 0 ↔ IsEmpty ι

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
h : lsub f = 0
i : ι
this : 0 < 0
⊢ False

Tactic:
exact this.false

Result:
no goals

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
h : lsub f = 0
i : ι
this : 0 < lsub f
⊢ False

Tactic:
rw [h] at this

Result:
ι : Type u
f : ι → Ordinal.{max u v}
h : lsub f = 0
i : ι
this : 0 < 0
⊢ False

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
h : lsub f = 0
i : ι
⊢ False

Tactic:
have := @lsub_pos.{_, v} _ ⟨i⟩ f

Result:
ι : Type u
f : ι → Ordinal.{max u v}
h : lsub f = 0
i : ι
this : 0 < lsub f
⊢ False

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ lsub f = 0 ↔ IsEmpty ι

Tactic:
refine ⟨fun h => ⟨fun i => ?_⟩, fun h => @lsub_empty _ h _⟩

Result:
ι : Type u
f : ι → Ordinal.{max u v}
h : lsub f = 0
i : ι
⊢ False
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- If `m ≠ 0` and the `Finset` of prime factors of `m` is contained in `s`, then `m`
is `s`-factored. -/
lemma mem_factoredNumbers_of_primeFactors_subset {s : Finset ℕ} {m : ℕ} (hm : m ≠ 0)
    (hp : m.primeFactors ⊆ s) :
    m ∈ factoredNumbers s

Proof state:
s : Finset ℕ
m : ℕ
hm : m ≠ 0
hp : m.primeFactors ⊆ s
⊢ m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s

Tactic:
exact ⟨hm, fun p hp' ↦ hp <| mem_primeFactors_iff_mem_primeFactorsList.mpr hp'⟩

Result:
no goals

Proof state:
s : Finset ℕ
m : ℕ
hm : m ≠ 0
hp : m.primeFactors ⊆ s
⊢ m ∈ factoredNumbers s

Tactic:
rw [mem_factoredNumbers]

Result:
s : Finset ℕ
m : ℕ
hm : m ≠ 0
hp : m.primeFactors ⊆ s
⊢ m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s
-- Mathlib/CategoryTheory/Simple.lean
theorem cokernel_zero_of_nonzero_to_simple {X Y : C} [Simple Y] {f : X ⟶ Y} (w : f ≠ 0) :
    cokernel.π f = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
⊢ cokernel.π f = 0

Tactic:
classical
  by_contra h
  haveI := isIso_of_epi_of_nonzero h
  exact w (eq_zero_of_mono_cokernel f)

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
h : ¬cokernel.π f = 0
this : IsIso (cokernel.π f)
⊢ False

Tactic:
exact w (eq_zero_of_mono_cokernel f)

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
⊢ cokernel.π f = 0

Tactic:
by_contra h

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
h : ¬cokernel.π f = 0
⊢ False

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
h : ¬cokernel.π f = 0
⊢ False

Tactic:
haveI := isIso_of_epi_of_nonzero h

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
h : ¬cokernel.π f = 0
this : IsIso (cokernel.π f)
⊢ False
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem list_cycles_perm_list_cycles {α : Type*} [Finite α] {l₁ l₂ : List (Perm α)}
    (h₀ : l₁.prod = l₂.prod) (h₁l₁ : ∀ σ : Perm α, σ ∈ l₁ → σ.IsCycle)
    (h₁l₂ : ∀ σ : Perm α, σ ∈ l₂ → σ.IsCycle) (h₂l₁ : l₁.Pairwise Disjoint)
    (h₂l₂ : l₂.Pairwise Disjoint) : l₁ ~ l₂

Proof state:
case pos
α : Type u_4
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : σ.IsCycle
⊢ σ ∈ l₁ ↔ σ ∈ l₂

Tactic:
obtain _ := not_forall.mp (mt ext hσ.ne_one)

Result:
case pos
α : Type u_4
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : σ.IsCycle
x✝ : ∃ x, ¬σ x = 1 x
⊢ σ ∈ l₁ ↔ σ ∈ l₂

Proof state:
α : Type u_4
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
⊢ σ ∈ l₁ ↔ σ ∈ l₂

Tactic:
by_cases hσ : σ.IsCycle

Result:
case pos
α : Type u_4
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : σ.IsCycle
⊢ σ ∈ l₁ ↔ σ ∈ l₂

case neg
α : Type u_4
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : ¬σ.IsCycle
⊢ σ ∈ l₁ ↔ σ ∈ l₂

Proof state:
case pos
α : Type u_4
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : σ.IsCycle
x✝ : ∃ x, ¬σ x = 1 x
⊢ σ ∈ l₁ ↔ σ ∈ l₂

Tactic:
rw [mem_list_cycles_iff h₁l₁ h₂l₁, mem_list_cycles_iff h₁l₂ h₂l₂, h₀]

Result:
no goals

Proof state:
case neg
α : Type u_4
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : ¬σ.IsCycle
⊢ σ ∈ l₁ ↔ σ ∈ l₂

Tactic:
exact iff_of_false (mt (h₁l₁ σ) hσ) (mt (h₁l₂ σ) hσ)

Result:
no goals

Proof state:
α : Type u_4
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
⊢ l₁ ~ l₂

Tactic:
refine
  (List.perm_ext_iff_of_nodup (nodup_of_pairwise_disjoint_cycles h₁l₁ h₂l₁)
        (nodup_of_pairwise_disjoint_cycles h₁l₂ h₂l₂)).mpr
    fun σ => ?_

Result:
α : Type u_4
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
⊢ σ ∈ l₁ ↔ σ ∈ l₂
-- Mathlib/Data/Nat/Init.lean
lemma sq_sub_sq (a b : ℕ) : a ^ 2 - b ^ 2 = (a + b) * (a - b)

Proof state:
a b : ℕ
⊢ a ^ 2 - b ^ 2 = (a + b) * (a - b)

Tactic:
simpa [Nat.pow_succ] using Nat.mul_self_sub_mul_self_eq a b

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
@[simp] lemma mk'_zero (d) (h : d ≠ 0) (w) : mk' 0 d h w = 0

Proof state:
case e_den
d : ℕ
h : d ≠ 0
w : (Int.natAbs 0).Coprime d
⊢ d = 1

Tactic:
simp_all

Result:
no goals

Proof state:
d : ℕ
h : d ≠ 0
w : (Int.natAbs 0).Coprime d
⊢ { num := 0, den := d, den_nz := h, reduced := w } = 0

Tactic:
congr

Result:
case e_den
d : ℕ
h : d ≠ 0
w : (Int.natAbs 0).Coprime d
⊢ d = 1
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem factorization_one : factorization 1 = 0

Proof state:
⊢ factorization 1 = 0

Tactic:
ext

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

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

Tactic:
simp [factorization]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Convolution.lean
theorem zero_mconv (μ : Measure M) : μ ∗ (0 : Measure M) = (0 : Measure M)

Proof state:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : MeasurableSpace M
μ : Measure M
⊢ μ ∗ 0 = 0

Tactic:
unfold mconv

Result:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : MeasurableSpace M
μ : Measure M
⊢ map (fun x => x.1 * x.2) (μ.prod 0) = 0

Proof state:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : MeasurableSpace M
μ : Measure M
⊢ map (fun x => x.1 * x.2) (μ.prod 0) = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Control/Bifunctor.lean
theorem fst_snd {α₀ α₁ β₀ β₁} (f : α₀ → α₁) (f' : β₀ → β₁) (x : F α₀ β₀) :
    fst f (snd f' x) = bimap f f' x

Proof state:
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α₀ α₁ : Type u₀
β₀ β₁ : Type u₁
f : α₀ → α₁
f' : β₀ → β₁
x : F α₀ β₀
⊢ fst f (snd f' x) = bimap f f' x

Tactic:
simp [fst, bimap_bimap]

Result:
no goals
-- Mathlib/Data/DFinsupp/Ext.lean
theorem addHom_ext {γ : Type w} [AddZeroClass γ] ⦃f g : (Π₀ i, β i) →+ γ⦄
    (H : ∀ (i : ι) (y : β i), f (single i y) = g (single i y)) : f = g

Proof state:
case intro.intro
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
γ : Type w
inst✝ : AddZeroClass γ
f g : (Π₀ (i : ι), β i) →+ γ
H : ∀ (i : ι) (y : β i), f (single i y) = g (single i y)
x : ι
y : β x
⊢ f (single x y) = g (single x y)

Tactic:
apply H

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
γ : Type w
inst✝ : AddZeroClass γ
f✝ g : (Π₀ (i : ι), β i) →+ γ
H : ∀ (i : ι) (y : β i), f✝ (single i y) = g (single i y)
f : Π₀ (i : ι), β i
hf : ∃ i y, single i y = f
⊢ f✝ f = g f

Tactic:
rcases hf with ⟨x, y, rfl⟩

Result:
case intro.intro
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
γ : Type w
inst✝ : AddZeroClass γ
f g : (Π₀ (i : ι), β i) →+ γ
H : ∀ (i : ι) (y : β i), f (single i y) = g (single i y)
x : ι
y : β x
⊢ f (single x y) = g (single x y)

Proof state:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
γ : Type w
inst✝ : AddZeroClass γ
f g : (Π₀ (i : ι), β i) →+ γ
H : ∀ (i : ι) (y : β i), f (single i y) = g (single i y)
⊢ f = g

Tactic:
refine AddMonoidHom.eq_of_eqOn_denseM add_closure_iUnion_range_single fun f hf => ?_

Result:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
γ : Type w
inst✝ : AddZeroClass γ
f✝ g : (Π₀ (i : ι), β i) →+ γ
H : ∀ (i : ι) (y : β i), f✝ (single i y) = g (single i y)
f : Π₀ (i : ι), β i
hf : f ∈ ⋃ i, Set.range (single i)
⊢ f✝ f = g f

Proof state:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
γ : Type w
inst✝ : AddZeroClass γ
f✝ g : (Π₀ (i : ι), β i) →+ γ
H : ∀ (i : ι) (y : β i), f✝ (single i y) = g (single i y)
f : Π₀ (i : ι), β i
hf : f ∈ ⋃ i, Set.range (single i)
⊢ f✝ f = g f

Tactic:
simp only [Set.mem_iUnion, Set.mem_range] at hf

Result:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
γ : Type w
inst✝ : AddZeroClass γ
f✝ g : (Π₀ (i : ι), β i) →+ γ
H : ∀ (i : ι) (y : β i), f✝ (single i y) = g (single i y)
f : Π₀ (i : ι), β i
hf : ∃ i y, single i y = f
⊢ f✝ f = g f
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma nonsingular_some (X Y : R) : W'.Nonsingular ![X, Y, 1] ↔ W'.toAffine.Nonsingular X Y

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
X Y : R
h :
  Y ^ 2 + (toAffine W').a₁ * X * Y + (toAffine W').a₃ * Y -
      (X ^ 3 + (toAffine W').a₂ * X ^ 2 + (toAffine W').a₄ * X + (toAffine W').a₆) =
    0
hX : W'.a₁ * Y - (3 * X ^ 2 + 2 * W'.a₂ * X + W'.a₄) = 0
hY : 2 * Y + (toAffine W').a₁ * X + (toAffine W').a₃ = 0
⊢ W'.a₁ * X * Y + 3 * W'.a₃ * Y - (2 * W'.a₂ * X ^ 2 + 4 * W'.a₄ * X + 6 * W'.a₆) = 0

Tactic:
linear_combination (norm := ring1) 6 * h - 2 * X * hX - 3 * Y * hY

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
X Y : R
⊢ Y ^ 2 + (toAffine W').a₁ * X * Y + (toAffine W').a₃ * Y -
        (X ^ 3 + (toAffine W').a₂ * X ^ 2 + (toAffine W').a₄ * X + (toAffine W').a₆) =
      0 →
    W'.a₁ * Y - (3 * X ^ 2 + 2 * W'.a₂ * X + W'.a₄) = 0 →
      2 * Y + (toAffine W').a₁ * X + (toAffine W').a₃ = 0 →
        W'.a₁ * X * Y + 3 * W'.a₃ * Y - (2 * W'.a₂ * X ^ 2 + 4 * W'.a₄ * X + 6 * W'.a₆) = 0

Tactic:
intro h hX hY

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
X Y : R
h :
  Y ^ 2 + (toAffine W').a₁ * X * Y + (toAffine W').a₃ * Y -
      (X ^ 3 + (toAffine W').a₂ * X ^ 2 + (toAffine W').a₄ * X + (toAffine W').a₆) =
    0
hX : W'.a₁ * Y - (3 * X ^ 2 + 2 * W'.a₂ * X + W'.a₄) = 0
hY : 2 * Y + (toAffine W').a₁ * X + (toAffine W').a₃ = 0
⊢ W'.a₁ * X * Y + 3 * W'.a₃ * Y - (2 * W'.a₂ * X ^ 2 + 4 * W'.a₄ * X + 6 * W'.a₆) = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
X Y : R
⊢ W'.Nonsingular ![X, Y, 1] ↔ (toAffine W').Nonsingular X Y

Tactic:
simp_rw [nonsingular_iff, equation_some, fin3_def_ext, Affine.nonsingular_iff',
  Affine.equation_iff', and_congr_right_iff, ← not_and_or, not_iff_not, one_pow, mul_one,
  and_congr_right_iff, Iff.comm, iff_self_and]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
X Y : R
⊢ Y ^ 2 + (toAffine W').a₁ * X * Y + (toAffine W').a₃ * Y -
        (X ^ 3 + (toAffine W').a₂ * X ^ 2 + (toAffine W').a₄ * X + (toAffine W').a₆) =
      0 →
    W'.a₁ * Y - (3 * X ^ 2 + 2 * W'.a₂ * X + W'.a₄) = 0 →
      2 * Y + (toAffine W').a₁ * X + (toAffine W').a₃ = 0 →
        W'.a₁ * X * Y + 3 * W'.a₃ * Y - (2 * W'.a₂ * X ^ 2 + 4 * W'.a₄ * X + 6 * W'.a₆) = 0
-- Mathlib/Analysis/Convex/Deriv.lean
lemma slope_lt_of_hasDerivAt (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hfd : HasDerivAt f f' x) :
    slope f x y < f'

Proof state:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : HasDerivAt f f' x
⊢ slope f x y < f'

Tactic:
simpa only [Pi.neg_def, slope_neg, neg_neg] using
  neg_lt_neg (hfc.neg.lt_slope_of_hasDerivAt hx hy hxy hfd.neg)

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem edges_nodup_of_support_nodup {u v : V} {p : G.Walk u v} (h : p.support.Nodup) :
    p.edges.Nodup

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
h : nil.support.Nodup
⊢ nil.edges.Nodup

Tactic:
simp

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.support.Nodup → p'.edges.Nodup
h : (cons h✝ p').support.Nodup
⊢ (cons h✝ p').edges.Nodup

Tactic:
simp only [edges_cons, support_cons, List.nodup_cons] at h ⊢

Result:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.support.Nodup → p'.edges.Nodup
h : u✝ ∉ p'.support ∧ p'.support.Nodup
⊢ s(u✝, v✝) ∉ p'.edges ∧ p'.edges.Nodup

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.support.Nodup → p'.edges.Nodup
h : u✝ ∉ p'.support ∧ p'.support.Nodup
⊢ s(u✝, v✝) ∉ p'.edges ∧ p'.edges.Nodup

Tactic:
exact ⟨fun h' => h.1 (fst_mem_support_of_mem_edges p' h'), ih h.2⟩

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.support.Nodup
⊢ p.edges.Nodup

Tactic:
induction p with
| nil => simp
| cons _ p' ih =>
  simp only [edges_cons, support_cons, List.nodup_cons] at h ⊢
  exact ⟨fun h' => h.1 (fst_mem_support_of_mem_edges p' h'), ih h.2⟩

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_δ'' {n} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ Fin.castSucc j) :
    X.δ (i.castLT (Nat.lt_of_le_of_lt (Fin.le_iff_val_le_val.mp H) j.is_lt)) ≫ X.δ j.succ =
      X.δ j ≫ X.δ i

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ X.map (SimplexCategory.δ (i.castLT ⋯)) ≫ X.map (SimplexCategory.δ j.succ) =
    X.map (SimplexCategory.δ j) ≫ X.map (SimplexCategory.δ i)

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ'' H]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ X.δ (i.castLT ⋯) ≫ X.δ j.succ = X.δ j ≫ X.δ i

Tactic:
dsimp [δ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ X.map (SimplexCategory.δ (i.castLT ⋯)) ≫ X.map (SimplexCategory.δ j.succ) =
    X.map (SimplexCategory.δ j) ≫ X.map (SimplexCategory.δ i)
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem le_pow_of_le_ramificationIdx {n : ℕ} (hn : n ≤ ramificationIdx f p P) :
    map f p ≤ P ^ n

Proof state:
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
n : ℕ
hn : ¬map f p ≤ P ^ n
⊢ ramificationIdx f p P < n

Tactic:
exact ramificationIdx_lt hn

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
n : ℕ
hn : n ≤ ramificationIdx f p P
⊢ map f p ≤ P ^ n

Tactic:
contrapose! hn

Result:
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
n : ℕ
hn : ¬map f p ≤ P ^ n
⊢ ramificationIdx f p P < n
-- Mathlib/Analysis/Calculus/LineDeriv/IntegrationByParts.lean
lemma integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1 [SigmaFinite μ]
    {f f' : E × ℝ → F} {g g' : E × ℝ → G} {B : F →L[ℝ] G →L[ℝ] W}
    (hf'g : Integrable (fun x ↦ B (f' x) (g x)) (μ.prod volume))
    (hfg' : Integrable (fun x ↦ B (f x) (g' x)) (μ.prod volume))
    (hfg : Integrable (fun x ↦ B (f x) (g x)) (μ.prod volume))
    (hf : ∀ x, HasLineDerivAt ℝ f (f' x) x (0, 1)) (hg : ∀ x, HasLineDerivAt ℝ g (g' x) x (0, 1)) :
    ∫ x, B (f x) (g' x) ∂(μ.prod volume) = - ∫ x, B (f' x) (g x) ∂(μ.prod volume) := calc
  ∫ x, B (f x) (g' x) ∂(μ.prod volume)
    = ∫ x, (∫ t, B (f (x, t)) (g' (x, t))) ∂μ := integral_prod _ hfg'
  _ = ∫ x, (- ∫ t, B (f' (x, t)) (g (x, t))) ∂μ

Proof state:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx : Integrable (fun y => (B (f' (x, y))) (g (x, y))) volume
hfg'x : Integrable (fun y => (B (f (x, y))) (g' (x, y))) volume
hfgx : Integrable (fun y => (B (f (x, y))) (g (x, y))) volume
t : ℝ
⊢ 0 = id t + -t

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
theorem incMatrix_of_not_mem_incidenceSet (h : e ∉ G.incidenceSet a) : G.incMatrix R a e = 0

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a : α
e : Sym2 α
h : e ∉ G.incidenceSet a
⊢ incMatrix R G a e = 0

Tactic:
rw [incMatrix_apply, Set.indicator_of_not_mem h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_insertₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    (h : Raw.WFImp m.1) {a : α} {b : β a} : Raw.WFImp (m.insertₘ a b).1

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

Tactic:
apply wfImp_replaceₘ _ h

Result:
no goals

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

Tactic:
rw [insertₘ]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ Raw.WFImp (if m.containsₘ a = true then m.replaceₘ a b else (m.consₘ a b).expandIfNecessary).val

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

Tactic:
apply wfImp_consₘ _ h _ _ (by simp_all)

Result:
no goals

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

Tactic:
simp_all

Result:
no goals

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

Tactic:
split

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

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

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

Tactic:
apply wfImp_expandIfNecessary

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