harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean
theorem biprodComparison'_comp_biprodComparison :
    biprodComparison' F X Y ≫ biprodComparison F X Y = 𝟙 (F.obj X ⊞ F.obj Y)

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : F.PreservesZeroMorphisms
⊢ F.biprodComparison' X Y ≫ F.biprodComparison X Y = 𝟙 (F.obj X ⊞ F.obj Y)

Tactic:
ext <;> simp [← Functor.map_comp]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integral_withDensity_eq_integral_smul {f : X → ℝ≥0} (f_meas : Measurable f) (g : X → E) :
    ∫ x, g x ∂μ.withDensity (fun x => f x) = ∫ x, f x • g x ∂μ

Proof state:
case pos
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x => ↑(f x))
⊢ (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ

case neg
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : ¬Integrable g (μ.withDensity fun x => ↑(f x))
⊢ (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ

Tactic:
swap

Result:
case neg
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : ¬Integrable g (μ.withDensity fun x => ↑(f x))
⊢ (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ

case pos
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x => ↑(f x))
⊢ (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ

Proof state:
case pos.refine_1
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x => ↑(f x))
c : E
s : Set X
s_meas : MeasurableSet s
hs : (μ.withDensity fun x => ↑(f x)) s < ⊤
⊢ 0 ≤ ∫ (a : X) in s, ↑(f a) ∂μ

Tactic:
exact integral_nonneg fun x => NNReal.coe_nonneg _

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem card_roots_of_disc_ne_zero [DecidableEq K] (ha : P.a ≠ 0) (h3 : (map φ P).roots = {x, y, z})
    (hd : P.disc ≠ 0) : (map φ P).roots.toFinset.card = 3

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝² : Field F
inst✝¹ : Field K
φ : F →+* K
x y z : K
inst✝ : DecidableEq K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
hd : P.disc ≠ 0
⊢ (map φ P).roots.toFinset.card = 3

Tactic:
rw [toFinset_card_of_nodup <| (disc_ne_zero_iff_roots_nodup ha h3).mp hd,
  ← splits_iff_card_roots ha, splits_iff_roots_eq_three ha]

Result:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝² : Field F
inst✝¹ : Field K
φ : F →+* K
x y z : K
inst✝ : DecidableEq K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
hd : P.disc ≠ 0
⊢ ∃ x y z, (map φ P).roots = {x, y, z}

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝² : Field F
inst✝¹ : Field K
φ : F →+* K
x y z : K
inst✝ : DecidableEq K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
hd : P.disc ≠ 0
⊢ ∃ x y z, (map φ P).roots = {x, y, z}

Tactic:
exact ⟨x, ⟨y, ⟨z, h3⟩⟩⟩

Result:
no goals
-- Mathlib/Analysis/Normed/Group/InfiniteSum.lean
theorem summable_iff_vanishing_norm [CompleteSpace E] {f : ι → E} :
    Summable f ↔ ∀ ε > (0 : ℝ), ∃ s : Finset ι, ∀ t, Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

Proof state:
ι : Type u_1
E : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : CompleteSpace E
f : ι → E
⊢ Summable f ↔ ∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

Tactic:
rw [summable_iff_cauchySeq_finset, cauchySeq_finset_iff_vanishing_norm]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem comapDomain_single (f : α → β) (a : α) (m : M)
    (hif : Set.InjOn f (f ⁻¹' (single (f a) m).support)) :
    comapDomain f (Finsupp.single (f a) m) hif = Finsupp.single a m

Proof state:
case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)
hm : m ≠ 0
⊢ comapDomain f (single (f a) m) hif = single a m

Tactic:
rw [eq_single_iff, comapDomain_apply, comapDomain_support, ← Finset.coe_subset, coe_preimage,
  support_single_ne_zero _ hm, coe_singleton, coe_singleton, single_eq_same]

Result:
case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)
hm : m ≠ 0
⊢ f ⁻¹' {f a} ⊆ {a} ∧ m = m

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)
⊢ comapDomain f (single (f a) m) hif = single a m

Tactic:
rcases eq_or_ne m 0 with (rfl | hm)

Result:
case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) 0).support)
⊢ comapDomain f (single (f a) 0) hif = single a 0

case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)
hm : m ≠ 0
⊢ comapDomain f (single (f a) m) hif = single a m

Proof state:
case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) 0).support)
⊢ comapDomain f (single (f a) 0) hif = single a 0

Tactic:
simp only [single_zero, comapDomain_zero]

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' {f a})
hm : m ≠ 0
⊢ f ⁻¹' {f a} ⊆ {a} ∧ m = m

Tactic:
exact ⟨fun x hx => hif hx rfl hx, rfl⟩

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)
hm : m ≠ 0
⊢ f ⁻¹' {f a} ⊆ {a} ∧ m = m

Tactic:
rw [support_single_ne_zero _ hm, coe_singleton] at hif

Result:
case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' {f a})
hm : m ≠ 0
⊢ f ⁻¹' {f a} ⊆ {a} ∧ m = m
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem map_eq_zero {S : Type*} [DivisionSemiring R] [Semiring S] [Nontrivial S]
    (φ : MvPowerSeries σ R) (f : R →+* S) : φ.map σ f = 0 ↔ φ = 0

Proof state:
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
φ : MvPowerSeries σ R
f : R →+* S
⊢ (∀ (n : σ →₀ ℕ), (coeff S n) ((map σ f) φ) = (coeff S n) 0) ↔ ∀ (n : σ →₀ ℕ), (coeff R n) φ = (coeff R n) 0

Tactic:
congr! with n

Result:
case a.h.a
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
φ : MvPowerSeries σ R
f : R →+* S
n : σ →₀ ℕ
⊢ (coeff S n) ((map σ f) φ) = (coeff S n) 0 ↔ (coeff R n) φ = (coeff R n) 0

Proof state:
case a.h.a
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
φ : MvPowerSeries σ R
f : R →+* S
n : σ →₀ ℕ
⊢ (coeff S n) ((map σ f) φ) = (coeff S n) 0 ↔ (coeff R n) φ = (coeff R n) 0

Tactic:
simp

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
φ : MvPowerSeries σ R
f : R →+* S
⊢ (map σ f) φ = 0 ↔ φ = 0

Tactic:
simp only [MvPowerSeries.ext_iff]

Result:
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
φ : MvPowerSeries σ R
f : R →+* S
⊢ (∀ (n : σ →₀ ℕ), (coeff S n) ((map σ f) φ) = (coeff S n) 0) ↔ ∀ (n : σ →₀ ℕ), (coeff R n) φ = (coeff R n) 0
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma image_coe_Iio (x : ℝ) : Real.toEReal '' Iio x = Ioo ⊥ ↑x

Proof state:
x : ℝ
⊢ Ioo ⊥ ↑↑x = Ioo ⊥ ↑x

Tactic:
rfl

Result:
no goals

Proof state:
x : ℝ
⊢ WithBot.some '' (WithTop.some '' Iio x) = Ioo ⊥ ↑x

Tactic:
rw [WithTop.image_coe_Iio, WithBot.image_coe_Iio]

Result:
x : ℝ
⊢ Ioo ⊥ ↑↑x = Ioo ⊥ ↑x

Proof state:
x : ℝ
⊢ Real.toEReal '' Iio x = Ioo ⊥ ↑x

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Result:
x : ℝ
⊢ WithBot.some '' (WithTop.some '' Iio x) = Ioo ⊥ ↑x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_of_eq {l l' : List α} (h : l = l') {i : Nat} (w : i < l.length) :
    l[i] = l'[i]'(h ▸ w)

Proof state:
case refl
α : Type u_1
l : List α
i : Nat
w : i < l.length
⊢ l[i] = l[i]

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
l l' : List α
h : l = l'
i : Nat
w : i < l.length
⊢ l[i] = l'[i]

Tactic:
cases h

Result:
case refl
α : Type u_1
l : List α
i : Nat
w : i < l.length
⊢ l[i] = l[i]
-- Mathlib/Combinatorics/SetFamily/KruskalKatona.lean
/-- Applying a compression strictly decreases the measure. This helps show that "compress until we
can't any more" is a terminating process. -/
private lemma familyMeasure_compression_lt_familyMeasure {U V : Finset (Fin n)} {hU : U.Nonempty}
    {hV : V.Nonempty} (h : max' U hU < max' V hV) {𝒜 : Finset (Finset (Fin n))} (a : 𝓒 U V 𝒜 ≠ 𝒜) :
    familyMeasure (𝓒 U V 𝒜) < familyMeasure 𝒜

Proof state:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
⊢ ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q

Tactic:
simp_rw [mem_filter]

Result:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
⊢ ∀ (Q : Finset (Fin n)), Q ∈ 𝒜 ∧ compress U V Q ∉ 𝒜 → compress U V Q ≠ Q

Proof state:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
ne₂ : (filter (fun A => compress U V A ∉ 𝒜) 𝒜).Nonempty
A : Finset (Fin n)
hA : A ∈ filter (fun a => compress U V a ∉ 𝒜) 𝒜
⊢ ∑ a ∈ compress U V A, 2 ^ ↑a < ∑ a ∈ A, 2 ^ ↑a

Tactic:
simp_rw [← sum_image Fin.val_injective.injOn]

Result:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
ne₂ : (filter (fun A => compress U V A ∉ 𝒜) 𝒜).Nonempty
A : Finset (Fin n)
hA : A ∈ filter (fun a => compress U V a ∉ 𝒜) 𝒜
⊢ ∑ x ∈ image Fin.val (compress U V A), 2 ^ x < ∑ x ∈ image Fin.val A, 2 ^ x

Proof state:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
⊢ ∀ (Q : Finset (Fin n)), Q ∈ 𝒜 ∧ compress U V Q ∉ 𝒜 → compress U V Q ≠ Q

Tactic:
intro Q hQ h

Result:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h✝ : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
Q : Finset (Fin n)
hQ : Q ∈ 𝒜 ∧ compress U V Q ∉ 𝒜
h : compress U V Q = Q
⊢ False
-- Mathlib/Computability/RegularExpressions.lean
theorem add_rmatch_iff (P Q : RegularExpression α) (x : List α) :
    (P + Q).rmatch x ↔ P.rmatch x ∨ Q.rmatch x

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ (P Q : RegularExpression α), (P + Q).rmatch tail✝ = true ↔ P.rmatch tail✝ = true ∨ Q.rmatch tail✝ = true
P Q : RegularExpression α
⊢ (P.deriv head✝ + Q.deriv head✝).rmatch tail✝ = true ↔
    P.rmatch (head✝ :: tail✝) = true ∨ Q.rmatch (head✝ :: tail✝) = true

Tactic:
exact ih _ _

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
⊢ (P + Q).rmatch [] = true ↔ P.rmatch [] = true ∨ Q.rmatch [] = true

Tactic:
simp only [rmatch, matchEpsilon, Bool.or_eq_true_iff]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ (P Q : RegularExpression α), (P + Q).rmatch tail✝ = true ↔ P.rmatch tail✝ = true ∨ Q.rmatch tail✝ = true
P Q : RegularExpression α
⊢ (P + Q).rmatch (head✝ :: tail✝) = true ↔ P.rmatch (head✝ :: tail✝) = true ∨ Q.rmatch (head✝ :: tail✝) = true

Tactic:
rw [rmatch, deriv_add]

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ (P Q : RegularExpression α), (P + Q).rmatch tail✝ = true ↔ P.rmatch tail✝ = true ∨ Q.rmatch tail✝ = true
P Q : RegularExpression α
⊢ (P.deriv head✝ + Q.deriv head✝).rmatch tail✝ = true ↔
    P.rmatch (head✝ :: tail✝) = true ∨ Q.rmatch (head✝ :: tail✝) = true

Proof state:
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
x : List α
⊢ (P + Q).rmatch x = true ↔ P.rmatch x = true ∨ Q.rmatch x = true

Tactic:
induction' x with _ _ ih generalizing P Q

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
⊢ (P + Q).rmatch [] = true ↔ P.rmatch [] = true ∨ Q.rmatch [] = true

case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ (P Q : RegularExpression α), (P + Q).rmatch tail✝ = true ↔ P.rmatch tail✝ = true ∨ Q.rmatch tail✝ = true
P Q : RegularExpression α
⊢ (P + Q).rmatch (head✝ :: tail✝) = true ↔ P.rmatch (head✝ :: tail✝) = true ∨ Q.rmatch (head✝ :: tail✝) = true
-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.End_equiv_aux (f : S →ₐ[R] S ⊗ S ⧸ KaehlerDifferential.ideal R S ^ 2) :
    (Ideal.Quotient.mkₐ R (KaehlerDifferential.ideal R S).cotangentIdeal).comp f =
        IsScalarTower.toAlgHom R S _ ↔
      (TensorProduct.lmul' R : S ⊗[R] S →ₐ[R] S).kerSquareLift.comp f = AlgHom.id R S

Proof state:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
x : S
⊢ ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x =
      (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x ↔
    ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x

Tactic:
have e₁ : (TensorProduct.lmul' R : S ⊗[R] S →ₐ[R] S).kerSquareLift (f x) =
    KaehlerDifferential.quotientCotangentIdealRingEquiv R S
      (Ideal.Quotient.mk (KaehlerDifferential.ideal R S).cotangentIdeal <| f x) := by
  generalize f x = y; obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y; rfl

Result:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
x : S
e₁ :
  (TensorProduct.lmul' R).kerSquareLift (f x) =
    (quotientCotangentIdealRingEquiv R S) ((Ideal.Quotient.mk (ideal R S).cotangentIdeal) (f x))
⊢ ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x =
      (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x ↔
    ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x

Proof state:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
⊢ ∀ (a : S),
    ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) a =
        (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) a ↔
      ((TensorProduct.lmul' R).kerSquareLift.comp f) a = (AlgHom.id R S) a

Tactic:
intro x

Result:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
x : S
⊢ ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x =
      (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x ↔
    ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem multiset_prod_le_inf {s : Multiset (Ideal R)} : s.prod ≤ s.inf

Proof state:
case refine_2
R : Type u
inst✝ : CommSemiring R
s✝ : Multiset (Ideal R)
a : Ideal R
s : Multiset (Ideal R)
ih : s.prod ≤ s.inf
⊢ a * s.prod ≤ a ⊓ s.inf

Tactic:
exact le_trans mul_le_inf (inf_le_inf le_rfl ih)

Result:
no goals

Proof state:
case refine_1
R : Type u
inst✝ : CommSemiring R
s : Multiset (Ideal R)
⊢ Multiset.prod 0 ≤ Multiset.inf 0

Tactic:
rw [Multiset.inf_zero]

Result:
case refine_1
R : Type u
inst✝ : CommSemiring R
s : Multiset (Ideal R)
⊢ Multiset.prod 0 ≤ ⊤

Proof state:
case refine_2
R : Type u
inst✝ : CommSemiring R
s✝ : Multiset (Ideal R)
a : Ideal R
s : Multiset (Ideal R)
ih : s.prod ≤ s.inf
⊢ (a ::ₘ s).prod ≤ (a ::ₘ s).inf

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

Result:
case refine_2
R : Type u
inst✝ : CommSemiring R
s✝ : Multiset (Ideal R)
a : Ideal R
s : Multiset (Ideal R)
ih : s.prod ≤ s.inf
⊢ a * s.prod ≤ a ⊓ s.inf

Proof state:
case refine_2
R : Type u
inst✝ : CommSemiring R
s : Multiset (Ideal R)
⊢ ∀ (a : Ideal R) (s : Multiset (Ideal R)), s.prod ≤ s.inf → (a ::ₘ s).prod ≤ (a ::ₘ s).inf

Tactic:
intro a s ih

Result:
case refine_2
R : Type u
inst✝ : CommSemiring R
s✝ : Multiset (Ideal R)
a : Ideal R
s : Multiset (Ideal R)
ih : s.prod ≤ s.inf
⊢ (a ::ₘ s).prod ≤ (a ::ₘ s).inf

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Multiset (Ideal R)
⊢ s.prod ≤ s.inf

Tactic:
refine s.induction_on ?_ ?_

Result:
case refine_1
R : Type u
inst✝ : CommSemiring R
s : Multiset (Ideal R)
⊢ Multiset.prod 0 ≤ Multiset.inf 0

case refine_2
R : Type u
inst✝ : CommSemiring R
s : Multiset (Ideal R)
⊢ ∀ (a : Ideal R) (s : Multiset (Ideal R)), s.prod ≤ s.inf → (a ::ₘ s).prod ≤ (a ::ₘ s).inf

Proof state:
case refine_1
R : Type u
inst✝ : CommSemiring R
s : Multiset (Ideal R)
⊢ Multiset.prod 0 ≤ ⊤

Tactic:
exact le_top

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem bihimp_bihimp_self : a ⇔ b ⇔ a = b

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⇔ b ⇔ a = b

Tactic:
rw [bihimp_comm, bihimp_bihimp_cancel_left]

Result:
no goals
-- Mathlib/NumberTheory/FunctionField.lean
theorem inftyValuation.X : inftyValuationDef Fq RatFunc.X = Multiplicative.ofAdd (1 : ℤ)

Proof state:
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
⊢ inftyValuationDef Fq RatFunc.X = ↑(Multiplicative.ofAdd 1)

Tactic:
rw [inftyValuationDef, if_neg RatFunc.X_ne_zero, RatFunc.intDegree_X]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Zip.lean
theorem zip.go_decl_eq {aig : AIG α} (i) (hi) (lhs rhs : RefVec aig len)
    (s : RefVec aig i) (f : (aig : AIG α) → BinaryInput aig → Entrypoint α)
    [LawfulOperator α BinaryInput f] [chainable : LawfulZipOperator α f] :
    ∀ (idx : Nat) (h1) (h2), (go aig i s hi lhs rhs f).1.decls[idx]'h2 = aig.decls[idx]'h1

Proof state:
case isFalse
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
aig : AIG α
i : Nat
hi : i ≤ len
lhs rhs : aig.RefVec len
s : aig.RefVec i
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
res : RefVecEntry α len
h✝ : ¬i < len
hgo : { aig := aig, vec := ⋯ ▸ s } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Tactic:
rw [← hgo]

Result:
case isFalse
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
aig : AIG α
i : Nat
hi : i ≤ len
lhs rhs : aig.RefVec len
s : aig.RefVec i
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
res : RefVecEntry α len
h✝ : ¬i < len
hgo : { aig := aig, vec := ⋯ ▸ s } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < { aig := aig, vec := ⋯ ▸ s }.aig.decls.size),
    { aig := aig, vec := ⋯ ▸ s }.aig.decls[idx] = aig.decls[idx]
-- Mathlib/CategoryTheory/Monoidal/Bimod.lean
theorem whiskerLeft_comp_bimod {X Y Z : Mon_ C} (M : Bimod X Y) {N P Q : Bimod Y Z} (f : N ⟶ P)
    (g : P ⟶ Q) : whiskerLeft M (f ≫ g) = whiskerLeft M f ≫ whiskerLeft M g

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M : Bimod X Y
N P Q : Bimod Y Z
f : N ⟶ P
g : P ⟶ Q
⊢ M.whiskerLeft (f ≫ g) = M.whiskerLeft f ≫ M.whiskerLeft g

Tactic:
ext

Result:
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M : Bimod X Y
N P Q : Bimod Y Z
f : N ⟶ P
g : P ⟶ Q
⊢ (M.whiskerLeft (f ≫ g)).hom = (M.whiskerLeft f ≫ M.whiskerLeft g).hom

Proof state:
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M : Bimod X Y
N P Q : Bimod Y Z
f : N ⟶ P
g : P ⟶ Q
⊢ (M.whiskerLeft (f ≫ g)).hom = (M.whiskerLeft f ≫ M.whiskerLeft g).hom

Tactic:
apply Limits.coequalizer.hom_ext

Result:
case h.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M : Bimod X Y
N P Q : Bimod Y Z
f : N ⟶ P
g : P ⟶ Q
⊢ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ (M.whiskerLeft (f ≫ g)).hom =
    coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ (M.whiskerLeft f ≫ M.whiskerLeft g).hom

Proof state:
case h.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M : Bimod X Y
N P Q : Bimod Y Z
f : N ⟶ P
g : P ⟶ Q
⊢ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ (M.whiskerLeft (f ≫ g)).hom =
    coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ (M.whiskerLeft f ≫ M.whiskerLeft g).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc (attr := simp)]
lemma RightHomologyData.homologyIso_hom_comp_ι (h : S.RightHomologyData) :
    h.homologyIso.hom ≫ h.ι = S.homologyι ≫ h.opcyclesIso.hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ h.homologyIso.hom ≫ h.ι = S.homologyι ≫ h.opcyclesIso.hom

Tactic:
dsimp only [homologyι, homologyIso]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ (S.rightHomologyIso.symm ≪≫ h.rightHomologyIso).hom ≫ h.ι =
    (S.rightHomologyIso.inv ≫ S.rightHomologyι) ≫ h.opcyclesIso.hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ (S.rightHomologyIso.symm ≪≫ h.rightHomologyIso).hom ≫ h.ι =
    (S.rightHomologyIso.inv ≫ S.rightHomologyι) ≫ h.opcyclesIso.hom

Tactic:
simp only [Iso.trans_hom, Iso.symm_hom, assoc, rightHomologyIso_hom_comp_ι]

Result:
no goals