harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem ite_ae_eq_of_measure_zero {γ} (f : α → γ) (g : α → γ) (s : Set α) [DecidablePred (· ∈ s)]
    (hs_zero : μ s = 0) :
    (fun x => ite (x ∈ s) (f x) (g x)) =ᵐ[μ] g

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs_zero : μ s = 0
⊢ (fun x => if x ∈ s then f x else g x) =ᶠ[ae μ] g

Tactic:
have h_ss : sᶜ ⊆ { a : α | ite (a ∈ s) (f a) (g a) = g a } := fun x hx => by
  simp [(Set.mem_compl_iff _ _).mp hx]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs_zero : μ s = 0
h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}
⊢ (fun x => if x ∈ s then f x else g x) =ᶠ[ae μ] g

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs_zero : μ s = 0
h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}
⊢ {x | (fun x => (fun x => if x ∈ s then f x else g x) x = g x) x}ᶜ ⊆ sᶜᶜ

Tactic:
rwa [Set.compl_subset_compl]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs_zero : μ s = 0
x : α
hx : x ∈ sᶜ
⊢ x ∈ {a | (if a ∈ s then f a else g a) = g a}

Tactic:
simp [(Set.mem_compl_iff _ _).mp hx]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs_zero : μ s = 0
h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}
⊢ {x | (fun x => (fun x => if x ∈ s then f x else g x) x = g x) x}ᶜ ⊆ s

Tactic:
conv_rhs => rw [← compl_compl s]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs_zero : μ s = 0
h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}
⊢ {x | (fun x => (fun x => if x ∈ s then f x else g x) x = g x) x}ᶜ ⊆ sᶜᶜ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs_zero : μ s = 0
h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}
⊢ (fun x => if x ∈ s then f x else g x) =ᶠ[ae μ] g

Tactic:
refine measure_mono_null ?_ hs_zero

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs_zero : μ s = 0
h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}
⊢ {x | (fun x => (fun x => if x ∈ s then f x else g x) x = g x) x}ᶜ ⊆ s
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
@[fun_prop]
lemma Units.continuousOn_inv₀_spectrum (a : Aˣ) : ContinuousOn (· ⁻¹) (spectrum R (a : A)) :=
  continuousOn_inv₀.mono <| by
    simpa only [Set.subset_compl_singleton_iff] using spectrum.zero_not_mem R a.isUnit

Proof state:
R : Type u_3
A : Type u_4
inst✝⁴ : Semifield R
inst✝³ : Ring A
inst✝² : TopologicalSpace R
inst✝¹ : HasContinuousInv₀ R
inst✝ : Algebra R A
a : Aˣ
⊢ spectrum R ↑a ⊆ {0}ᶜ

Tactic:
simpa only [Set.subset_compl_singleton_iff] using spectrum.zero_not_mem R a.isUnit

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem nndist_integral_add_measure_le_lintegral
    {f : α → G} (h₁ : Integrable f μ) (h₂ : Integrable f ν) :
    (nndist (∫ x, f x ∂μ) (∫ x, f x ∂(μ + ν)) : ℝ≥0∞) ≤ ∫⁻ x, ‖f x‖ₑ ∂ν

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ ν : Measure α
f : α → G
h₁ : Integrable f μ
h₂ : Integrable f ν
⊢ ↑‖∫ (x : α), f x ∂ν‖₊ ≤ ∫⁻ (x : α), ‖f x‖ₑ ∂ν

Tactic:
exact enorm_integral_le_lintegral_enorm _

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ ν : Measure α
f : α → G
h₁ : Integrable f μ
h₂ : Integrable f ν
⊢ ↑(nndist (∫ (x : α), f x ∂μ) (∫ (x : α), f x ∂(μ + ν))) ≤ ∫⁻ (x : α), ‖f x‖ₑ ∂ν

Tactic:
rw [integral_add_measure h₁ h₂, nndist_comm, nndist_eq_nnnorm, add_sub_cancel_left]

Result:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ ν : Measure α
f : α → G
h₁ : Integrable f μ
h₂ : Integrable f ν
⊢ ↑‖∫ (x : α), f x ∂ν‖₊ ≤ ∫⁻ (x : α), ‖f x‖ₑ ∂ν
-- Mathlib/Order/Minimal.lean
theorem minimal_mem_image_iff (ha : a ∈ s) : Minimal (· ∈ f '' s) (f a) ↔ Minimal (· ∈ s) a :=
  _root_.minimal_mem_image_monotone_iff ha (by simp [f.le_iff_le])

Proof state:
α : Type u_1
a : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
f : α ↪o β
ha : a ∈ s
⊢ ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)

Tactic:
simp [f.le_iff_le]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addZ_of_Z_eq_zero_right [NoZeroDivisors R] {P Q : Fin 3 → R} (hQ : W'.Equation Q)
    (hQz : Q z = 0) : W'.addZ P Q = -(Q y ^ 2 * P z) * P z

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -3 * P x ^ 2 * 0 * 0 + 3 * P x * 0 ^ 2 * P z + P y ^ 2 * 0 ^ 2 - Q y ^ 2 * P z ^ 2 + W'.a₁ * P x * P y * 0 ^ 2 -
                  W'.a₁ * 0 * Q y * P z ^ 2 -
                W'.a₂ * P x ^ 2 * 0 ^ 2 +
              W'.a₂ * 0 ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * 0 ^ 2 -
          W'.a₃ * Q y * P z ^ 2 * 0 -
        W'.a₄ * P x * P z * 0 ^ 2 +
      W'.a₄ * 0 * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * P z

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ W'.addZ P Q = -(Q y ^ 2 * P z) * P z

Tactic:
rw [addZ, hQz, X_eq_zero_of_Z_eq_zero hQ hQz]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -3 * P x ^ 2 * 0 * 0 + 3 * P x * 0 ^ 2 * P z + P y ^ 2 * 0 ^ 2 - Q y ^ 2 * P z ^ 2 + W'.a₁ * P x * P y * 0 ^ 2 -
                  W'.a₁ * 0 * Q y * P z ^ 2 -
                W'.a₂ * P x ^ 2 * 0 ^ 2 +
              W'.a₂ * 0 ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * 0 ^ 2 -
          W'.a₃ * Q y * P z ^ 2 * 0 -
        W'.a₄ * P x * P z * 0 ^ 2 +
      W'.a₄ * 0 * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * P z
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatten_eq_empty_iff {L : Array (Array α)} : L.flatten = #[] ↔ ∀ l ∈ L, l = #[]

Proof state:
case of
α : Type u_1
xss✝ : List (List α)
⊢ (List.map List.toArray xss✝).toArray.flatten = #[] ↔
    ∀ (l : Array α), l ∈ (List.map List.toArray xss✝).toArray → l = #[]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
L : Array (Array α)
⊢ L.flatten = #[] ↔ ∀ (l : Array α), l ∈ L → l = #[]

Tactic:
induction L using array₂_induction

Result:
case of
α : Type u_1
xss✝ : List (List α)
⊢ (List.map List.toArray xss✝).toArray.flatten = #[] ↔
    ∀ (l : Array α), l ∈ (List.map List.toArray xss✝).toArray → l = #[]
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem right_eq_mul₀ (hb : b ≠ 0) : b = a * b ↔ a = 1

Proof state:
M₀ : Type u_1
inst✝ : CancelMonoidWithZero M₀
a b : M₀
hb : b ≠ 0
⊢ b = a * b ↔ a = 1

Tactic:
rw [eq_comm, mul_eq_right₀ hb]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiffAt.sum {ι : Type*} {f : ι → E → F} {s : Finset ι} {x : E}
    (h : ∀ i ∈ s, ContDiffAt 𝕜 n (fun x => f i x) x) :
    ContDiffAt 𝕜 n (fun x => ∑ i ∈ s, f i x) x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
ι : Type u_3
f : ι → E → F
s : Finset ι
x : E
h : ∀ i ∈ s, ContDiffAt 𝕜 n (fun x => f i x) x
⊢ ContDiffAt 𝕜 n (fun x => ∑ i ∈ s, f i x) x

Tactic:
rw [← contDiffWithinAt_univ] at *

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
ι : Type u_3
f : ι → E → F
s : Finset ι
x : E
h : ∀ i ∈ s, ContDiffAt 𝕜 n (fun x => f i x) x
⊢ ContDiffWithinAt 𝕜 n (fun x => ∑ i ∈ s, f i x) univ x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
ι : Type u_3
f : ι → E → F
s : Finset ι
x : E
h : ∀ i ∈ s, ContDiffAt 𝕜 n (fun x => f i x) x
⊢ ContDiffWithinAt 𝕜 n (fun x => ∑ i ∈ s, f i x) univ x

Tactic:
exact ContDiffWithinAt.sum h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem toList_zipIdx (a : Vector α n) (k : Nat := 0) :
    (a.zipIdx k).toList = a.toList.zipIdx k

Proof state:
α : Type u_1
n : Nat
a : Vector α n
k : optParam Nat 0
⊢ (a.zipIdx k).toList = a.toList.zipIdx k

Tactic:
rcases a with ⟨a, rfl⟩

Result:
case mk
α : Type u_1
k : optParam Nat 0
a : Array α
⊢ ({ toArray := a, size_toArray := ⋯ }.zipIdx k).toList = { toArray := a, size_toArray := ⋯ }.toList.zipIdx k

Proof state:
case mk
α : Type u_1
k : optParam Nat 0
a : Array α
⊢ ({ toArray := a, size_toArray := ⋯ }.zipIdx k).toList = { toArray := a, size_toArray := ⋯ }.toList.zipIdx k

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Comap.lean
theorem comap_comp (f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R)
    (g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R) : comap (g.comp f) = comap f ∘ comap g

Proof state:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
⊢ comap (g.comp f) = comap f ∘ comap g

Tactic:
funext x

Result:
case h
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
⊢ comap (g.comp f) x = (comap f ∘ comap g) x

Proof state:
case h
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
⊢ comap (g.comp f) x = (comap f ∘ comap g) x

Tactic:
exact comap_comp_apply _ _ _

Result:
no goals
-- Mathlib/Topology/Separation/CompletelyRegular.lean
lemma injective_stoneCechUnit_of_t35Space [T35Space X] :
    Function.Injective (stoneCechUnit : X → StoneCech X)

Proof state:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : T35Space X
a b : X
hab : stoneCechUnit a = stoneCechUnit b
⊢ a = b

Tactic:
contrapose hab

Result:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : T35Space X
a b : X
hab : ¬a = b
⊢ ¬stoneCechUnit a = stoneCechUnit b

Proof state:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : T35Space X
⊢ Function.Injective stoneCechUnit

Tactic:
intros a b hab

Result:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : T35Space X
a b : X
hab : stoneCechUnit a = stoneCechUnit b
⊢ a = b

Proof state:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : T35Space X
a b : X
hab : ¬a = b
⊢ ¬stoneCechUnit a = stoneCechUnit b

Tactic:
obtain ⟨f, fc, fab⟩ := separatesPoints_continuous_of_t35Space_Icc hab

Result:
case intro.intro
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : T35Space X
a b : X
hab : ¬a = b
f : X → ↑I
fc : f ∈ Continuous
fab : f a ≠ f b
⊢ ¬stoneCechUnit a = stoneCechUnit b

Proof state:
case intro.intro
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : T35Space X
a b : X
hab : ¬a = b
f : X → ↑I
fc : f ∈ Continuous
fab : f a ≠ f b
⊢ ¬stoneCechUnit a = stoneCechUnit b

Tactic:
exact fun q ↦ fab (eq_if_stoneCechUnit_eq fc q)

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
lemma exists_finiteIntegralAdele_iff (a : FiniteAdeleRing R K) :
    (∃ c : R_hat R K, a = c) ↔ ∀ v : HeightOneSpectrum R, a v ∈ adicCompletionIntegers K v :=
  ⟨by rintro ⟨c, rfl⟩ v; exact (c v).2, fun h ↦ ⟨fun v ↦ ⟨a v, h v⟩, rfl⟩⟩

Proof state:
case intro
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
c : R_hat R K
v : HeightOneSpectrum R
⊢ ↑c v ∈ adicCompletionIntegers K v

Tactic:
exact (c v).2

Result:
no goals

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : FiniteAdeleRing R K
⊢ (∃ c, a = ↑c) → ∀ (v : HeightOneSpectrum R), a v ∈ adicCompletionIntegers K v

Tactic:
rintro ⟨c, rfl⟩ v

Result:
case intro
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
c : R_hat R K
v : HeightOneSpectrum R
⊢ ↑c v ∈ adicCompletionIntegers K v
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem lt_cof_power {a b : Cardinal} (ha : ℵ₀ ≤ a) (b1 : 1 < b) : a < cof (b^a).ord

Proof state:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
b1 : 1 < b
b0 : b ≠ 0
⊢ b ^ a < (b ^ a) ^ (b ^ a).ord.cof

Tactic:
exact lt_power_cof (ha.trans <| (cantor' _ b1).le)

Result:
no goals

Proof state:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
b1 : 1 < b
b0 : b ≠ 0
⊢ a < (b ^ a).ord.cof

Tactic:
apply lt_imp_lt_of_le_imp_le (power_le_power_left <| power_ne_zero a b0)

Result:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
b1 : 1 < b
b0 : b ≠ 0
⊢ (b ^ a) ^ a < (b ^ a) ^ (b ^ a).ord.cof

Proof state:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
b1 : 1 < b
b0 : b ≠ 0
⊢ (b ^ a) ^ a < (b ^ a) ^ (b ^ a).ord.cof

Tactic:
rw [← power_mul, mul_eq_self ha]

Result:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
b1 : 1 < b
b0 : b ≠ 0
⊢ b ^ a < (b ^ a) ^ (b ^ a).ord.cof

Proof state:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
b1 : 1 < b
⊢ a < (b ^ a).ord.cof

Tactic:
have b0 : b ≠ 0 := (zero_lt_one.trans b1).ne'

Result:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
b1 : 1 < b
b0 : b ≠ 0
⊢ a < (b ^ a).ord.cof
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
protected lemma le_of_add_le_add_left [LE α] [AddLeftReflectLE α] (hx : x ≠ ⊥) :
    x + y ≤ x + z → y ≤ z

Proof state:
case intro
α : Type u
inst✝² : Add α
y z : WithBot α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x : α
⊢ ↑x + y ≤ ↑x + z → y ≤ z

Tactic:
cases y <;> cases z <;> simp [← coe_add]

Result:
case intro.coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝¹ a✝ : α
⊢ x + a✝¹ ≤ x + a✝ → a✝¹ ≤ a✝

Proof state:
α : Type u
inst✝² : Add α
x y z : WithBot α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
hx : x ≠ ⊥
⊢ x + y ≤ x + z → y ≤ z

Tactic:
lift x to α using hx

Result:
case intro
α : Type u
inst✝² : Add α
y z : WithBot α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x : α
⊢ ↑x + y ≤ ↑x + z → y ≤ z

Proof state:
case intro.coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝¹ a✝ : α
⊢ x + a✝¹ ≤ x + a✝ → a✝¹ ≤ a✝

Tactic:
simpa using le_of_add_le_add_left

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[reassoc]
lemma comp_liftCycles {A' : C} (α : A' ⟶ A) :
    α ≫ S.liftCycles k hk = S.liftCycles (α ≫ k) (by rw [assoc, hk, comp_zero])

Proof state:
C : Type u_1
inst✝² : Category.{?u.200331, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : S.HasLeftHomology
A' : C
α : A' ⟶ A
⊢ (α ≫ k) ≫ S.g = 0

Tactic:
rw [assoc, hk, comp_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : S.HasLeftHomology
A' : C
α : A' ⟶ A
⊢ α ≫ S.liftCycles k hk = S.liftCycles (α ≫ k) ⋯

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Prod.lean
theorem antidiagonal.fst_le {n : A} {kl : A × A} (hlk : kl ∈ antidiagonal n) : kl.1 ≤ n

Proof state:
A : Type u_1
inst✝² : OrderedAddCommMonoid A
inst✝¹ : CanonicallyOrderedAdd A
inst✝ : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ antidiagonal n
⊢ kl.1 ≤ n

Tactic:
rw [le_iff_exists_add]

Result:
A : Type u_1
inst✝² : OrderedAddCommMonoid A
inst✝¹ : CanonicallyOrderedAdd A
inst✝ : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ antidiagonal n
⊢ ∃ c, n = kl.1 + c

Proof state:
case h
A : Type u_1
inst✝² : OrderedAddCommMonoid A
inst✝¹ : CanonicallyOrderedAdd A
inst✝ : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ antidiagonal n
⊢ n = kl.1 + kl.2

Tactic:
rwa [mem_antidiagonal, eq_comm] at hlk

Result:
no goals

Proof state:
A : Type u_1
inst✝² : OrderedAddCommMonoid A
inst✝¹ : CanonicallyOrderedAdd A
inst✝ : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ antidiagonal n
⊢ ∃ c, n = kl.1 + c

Tactic:
use kl.2

Result:
case h
A : Type u_1
inst✝² : OrderedAddCommMonoid A
inst✝¹ : CanonicallyOrderedAdd A
inst✝ : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ antidiagonal n
⊢ n = kl.1 + kl.2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem exists_mem_of_size_eq_add_one {l : Array α} (h : l.size = n + 1) : ∃ a, a ∈ l

Proof state:
case mk
α : Type u_1
n : Nat
toList✝ : List α
h : { toList := toList✝ }.size = n + 1
⊢ ∃ a, a ∈ { toList := toList✝ }

Tactic:
simpa using List.exists_mem_of_length_eq_add_one h

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Array α
h : l.size = n + 1
⊢ ∃ a, a ∈ l

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
toList✝ : List α
h : { toList := toList✝ }.size = n + 1
⊢ ∃ a, a ∈ { toList := toList✝ }
-- Mathlib/Data/Nat/ModEq.lean
@[simp] lemma modEq_zero_iff : a ≡ b [MOD 0] ↔ a = b

Proof state:
a b : ℕ
⊢ a ≡ b [MOD 0] ↔ a = b

Tactic:
rw [ModEq, mod_zero, mod_zero]

Result:
no goals
-- Mathlib/ModelTheory/Satisfiability.lean
theorem exists_model_card_eq (h : ∃ M : ModelType.{u, v, max u v} T, Infinite M) (κ : Cardinal.{w})
    (h1 : ℵ₀ ≤ κ) (h2 : Cardinal.lift.{w} L.card ≤ Cardinal.lift.{max u v} κ) :
    ∃ N : ModelType.{u, v, w} T, #N = κ

Proof state:
case intro.intro.intro
L : Language
T : L.Theory
M : T.ModelType
MI this✝ : Infinite ↑M
N : Bundled L.Structure
hN : ↑M ≅[L] ↑N
h1 : ℵ₀ ≤ #↑N
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} #↑N
this : Nonempty ↑N
⊢ ∃ N_1, #↑N_1 = #↑N

Tactic:
exact ⟨hN.theory_model.bundled, rfl⟩

Result:
no goals

Proof state:
case intro
L : Language
T : L.Theory
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
M : T.ModelType
MI : Infinite ↑M
⊢ ∃ N, #↑N = κ

Tactic:
haveI := MI

Result:
case intro
L : Language
T : L.Theory
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
M : T.ModelType
MI this : Infinite ↑M
⊢ ∃ N, #↑N = κ

Proof state:
case intro.intro.intro
L : Language
T : L.Theory
M : T.ModelType
MI this : Infinite ↑M
N : Bundled L.Structure
hN : ↑M ≅[L] ↑N
h1 : ℵ₀ ≤ #↑N
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} #↑N
⊢ ∃ N_1, #↑N_1 = #↑N

Tactic:
haveI : Nonempty N := hN.nonempty

Result:
case intro.intro.intro
L : Language
T : L.Theory
M : T.ModelType
MI this✝ : Infinite ↑M
N : Bundled L.Structure
hN : ↑M ≅[L] ↑N
h1 : ℵ₀ ≤ #↑N
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} #↑N
this : Nonempty ↑N
⊢ ∃ N_1, #↑N_1 = #↑N

Proof state:
L : Language
T : L.Theory
h : ∃ M, Infinite ↑M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
⊢ ∃ N, #↑N = κ

Tactic:
cases h with
| intro M MI =>
  haveI := MI
  obtain ⟨N, hN, rfl⟩ := exists_elementarilyEquivalent_card_eq L M κ h1 h2
  haveI : Nonempty N := hN.nonempty
  exact ⟨hN.theory_model.bundled, rfl⟩

Result:
no goals

Proof state:
case intro
L : Language
T : L.Theory
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
M : T.ModelType
MI this : Infinite ↑M
⊢ ∃ N, #↑N = κ

Tactic:
obtain ⟨N, hN, rfl⟩ := exists_elementarilyEquivalent_card_eq L M κ h1 h2

Result:
case intro.intro.intro
L : Language
T : L.Theory
M : T.ModelType
MI this : Infinite ↑M
N : Bundled L.Structure
hN : ↑M ≅[L] ↑N
h1 : ℵ₀ ≤ #↑N
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} #↑N
⊢ ∃ N_1, #↑N_1 = #↑N
-- Mathlib/Data/Set/Image.lean
theorem image_subset_image_iff {f : α → β} (hf : Injective f) : f '' s ⊆ f '' t ↔ s ⊆ t

Proof state:
α : Type u_1
β : Type u_2
s t : Set α
f : α → β
hf : Injective f
h : f '' s ⊆ f '' t
⊢ s ⊆ t

Tactic:
rw [← preimage_image_eq s hf, ← preimage_image_eq t hf]

Result:
α : Type u_1
β : Type u_2
s t : Set α
f : α → β
hf : Injective f
h : f '' s ⊆ f '' t
⊢ f ⁻¹' (f '' s) ⊆ f ⁻¹' (f '' t)

Proof state:
α : Type u_1
β : Type u_2
s t : Set α
f : α → β
hf : Injective f
⊢ f '' s ⊆ f '' t ↔ s ⊆ t

Tactic:
refine Iff.symm <| (Iff.intro (image_subset f)) fun h => ?_

Result:
α : Type u_1
β : Type u_2
s t : Set α
f : α → β
hf : Injective f
h : f '' s ⊆ f '' t
⊢ s ⊆ t

Proof state:
α : Type u_1
β : Type u_2
s t : Set α
f : α → β
hf : Injective f
h : f '' s ⊆ f '' t
⊢ f ⁻¹' (f '' s) ⊆ f ⁻¹' (f '' t)

Tactic:
exact preimage_mono h

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem Commute.geom_sum₂_Ico [DivisionRing α] {x y : α} (h : Commute x y) (hxy : x ≠ y)
    {m n : ℕ} (hmn : m ≤ n) :
    (∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i)) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)

Proof state:
α : Type u
inst✝ : DivisionRing α
x y : α
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
⊢ ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)

Tactic:
have : x - y ≠ 0 := by simp_all [sub_eq_iff_eq_add]

Result:
α : Type u
inst✝ : DivisionRing α
x y : α
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
this : x - y ≠ 0
⊢ ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)

Proof state:
α : Type u
inst✝ : DivisionRing α
x y : α
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
this : x - y ≠ 0
⊢ ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)

Tactic:
rw [← h.geom_sum₂_Ico_mul hmn, mul_div_cancel_right₀ _ this]

Result:
no goals

Proof state:
α : Type u
inst✝ : DivisionRing α
x y : α
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
⊢ x - y ≠ 0

Tactic:
simp_all [sub_eq_iff_eq_add]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
theorem closure_pow (s : Set R) : ∀ n : ℕ, closure s ^ n = closure (s ^ n)
  | 0 => by rw [pow_zero, pow_zero, one_eq_closure_one_set]
  | n + 1 => by rw [pow_succ, pow_succ, closure_pow s n, closure_mul_closure]

Proof state:
R : Type u_4
inst✝ : Semiring R
s : Set R
n : ℕ
⊢ closure s ^ (n + 1) = closure (s ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ, closure_pow s n, closure_mul_closure]

Result:
no goals

Proof state:
R : Type u_4
inst✝ : Semiring R
s : Set R
⊢ closure s ^ 0 = closure (s ^ 0)

Tactic:
rw [pow_zero, pow_zero, one_eq_closure_one_set]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Basic.lean
theorem coe_prod {ι : Type*} [Fintype ι] (f : ι → S) : (↑(∏ i, f i) : L) = ∏ i, (f i : L)

Proof state:
case insert
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
S : IntermediateField K L
ι : Type u_4
inst✝ : Fintype ι
f : ι → ↥S
i : ι
s : Finset ι
hi : i ∉ s
H : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
⊢ ↑(∏ i ∈ insert i s, f i) = ∏ i ∈ insert i s, ↑(f i)

Tactic:
rw [Finset.prod_insert hi, MulMemClass.coe_mul, H, Finset.prod_insert hi]

Result:
no goals

Proof state:
case empty
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
S : IntermediateField K L
ι : Type u_4
inst✝ : Fintype ι
f : ι → ↥S
⊢ ↑(∏ i ∈ ∅, f i) = ∏ i ∈ ∅, ↑(f i)

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
S : IntermediateField K L
ι : Type u_4
inst✝ : Fintype ι
f : ι → ↥S
⊢ ↑(∏ i : ι, f i) = ∏ i : ι, ↑(f i)

Tactic:
induction' (Finset.univ : Finset ι) using Finset.induction_on with i s hi H

Result:
case empty
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
S : IntermediateField K L
ι : Type u_4
inst✝ : Fintype ι
f : ι → ↥S
⊢ ↑(∏ i ∈ ∅, f i) = ∏ i ∈ ∅, ↑(f i)

case insert
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
S : IntermediateField K L
ι : Type u_4
inst✝ : Fintype ι
f : ι → ↥S
i : ι
s : Finset ι
hi : i ∉ s
H : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
⊢ ↑(∏ i ∈ insert i s, f i) = ∏ i ∈ insert i s, ↑(f i)