harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem AddValuation.map_mul (x y : ℚ_[p]) :
    addValuationDef (x * y : ℚ_[p]) = addValuationDef x + addValuationDef y

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
⊢ (if x * y = 0 then ⊤ else ↑(x * y).valuation) =
    (if x = 0 then ⊤ else ↑x.valuation) + if y = 0 then ⊤ else ↑y.valuation

Tactic:
by_cases hy : y = 0

Result:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
hy : y = 0
⊢ (if x * y = 0 then ⊤ else ↑(x * y).valuation) =
    (if x = 0 then ⊤ else ↑x.valuation) + if y = 0 then ⊤ else ↑y.valuation

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then ⊤ else ↑(x * y).valuation) =
    (if x = 0 then ⊤ else ↑x.valuation) + if y = 0 then ⊤ else ↑y.valuation

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then ⊤ else ↑(x * y).valuation) =
    (if x = 0 then ⊤ else ↑x.valuation) + if y = 0 then ⊤ else ↑y.valuation

Tactic:
rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe,
  valuation_mul hx hy]

Result:
no goals

Proof state:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x = 0
⊢ (if x * y = 0 then ⊤ else ↑(x * y).valuation) =
    (if x = 0 then ⊤ else ↑x.valuation) + if y = 0 then ⊤ else ↑y.valuation

Tactic:
rw [hx, if_pos rfl, zero_mul, if_pos rfl, WithTop.top_add]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ (x * y).addValuationDef = x.addValuationDef + y.addValuationDef

Tactic:
simp only [addValuationDef]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ (if x * y = 0 then ⊤ else ↑(x * y).valuation) =
    (if x = 0 then ⊤ else ↑x.valuation) + if y = 0 then ⊤ else ↑y.valuation

Proof state:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
hy : y = 0
⊢ (if x * y = 0 then ⊤ else ↑(x * y).valuation) =
    (if x = 0 then ⊤ else ↑x.valuation) + if y = 0 then ⊤ else ↑y.valuation

Tactic:
rw [hy, if_pos rfl, mul_zero, if_pos rfl, WithTop.add_top]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ (if x * y = 0 then ⊤ else ↑(x * y).valuation) =
    (if x = 0 then ⊤ else ↑x.valuation) + if y = 0 then ⊤ else ↑y.valuation

Tactic:
by_cases hx : x = 0

Result:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x = 0
⊢ (if x * y = 0 then ⊤ else ↑(x * y).valuation) =
    (if x = 0 then ⊤ else ↑x.valuation) + if y = 0 then ⊤ else ↑y.valuation

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
⊢ (if x * y = 0 then ⊤ else ↑(x * y).valuation) =
    (if x = 0 then ⊤ else ↑x.valuation) + if y = 0 then ⊤ else ↑y.valuation
-- Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
theorem spanNorm_mul_of_bot_or_top (eq_bot_or_top : ∀ I : Ideal R, I = ⊥ ∨ I = ⊤) (I J : Ideal S) :
    spanNorm R (I * J) = spanNorm R I * spanNorm R J

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
⊢ spanNorm R (I * J) = spanNorm R I * spanNorm R J

Tactic:
refine le_antisymm ?_ (spanNorm_mul_spanNorm_le R _ _)

Result:
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
⊢ spanNorm R (I * J) ≤ spanNorm R I * spanNorm R J
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem nfp_add_eq_mul_omega0 {a b} (hba : b ≤ a * ω) : nfp (a + ·) b = a * ω

Proof state:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a + a * ω ≤ a * ω

Tactic:
rw [← mul_one_add, one_add_omega0]

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ nfp (fun x => a + x) 0 ≤ nfp (fun x => a + x) b

Tactic:
exact nfp_monotone (isNormal_add_right a).monotone (Ordinal.zero_le b)

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ nfp (fun x => a + x) b = a * ω

Tactic:
apply le_antisymm (nfp_le_fp (isNormal_add_right a).monotone hba _)

Result:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a * ω ≤ nfp (fun x => a + x) b

a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a + a * ω ≤ a * ω

Proof state:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a * ω ≤ nfp (fun x => a + x) b

Tactic:
rw [← nfp_add_zero]

Result:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ nfp (fun x => a + x) 0 ≤ nfp (fun x => a + x) b
-- Mathlib/Data/Matroid/Circuit.lean
lemma IsCircuit.isBasis_iff_eq_diff_singleton (hC : M.IsCircuit C) :
    M.IsBasis I C ↔ ∃ e ∈ C, I = C \ {e}

Proof state:
case refine_2
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
⊢ (∃ e ∈ C, I = C \ {e}) → M.IsBasis I C

Tactic:
rintro ⟨e, he, rfl⟩

Result:
case refine_2.intro.intro
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
he : e ∈ C
⊢ M.IsBasis (C \ {e}) C

Proof state:
case refine_1
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
h : M.IsBasis I C
⊢ ∃ e ∈ C, I = C \ {e}

Tactic:
obtain ⟨e, he⟩ := exists_of_ssubset
  (h.subset.ssubset_of_ne (by rintro rfl; exact hC.dep.not_indep h.indep))

Result:
case refine_1.intro
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
h : M.IsBasis I C
e : α
he : e ∈ C ∧ e ∉ I
⊢ ∃ e ∈ C, I = C \ {e}

Proof state:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
⊢ M.IsBasis I C ↔ ∃ e ∈ C, I = C \ {e}

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Result:
case refine_1
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
h : M.IsBasis I C
⊢ ∃ e ∈ C, I = C \ {e}

case refine_2
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
⊢ (∃ e ∈ C, I = C \ {e}) → M.IsBasis I C

Proof state:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
h : M.IsBasis I C
⊢ I ≠ C

Tactic:
rintro rfl

Result:
α : Type u_1
M : Matroid α
I : Set α
hC : M.IsCircuit I
h : M.IsBasis I I
⊢ False

Proof state:
case refine_1.intro
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
h : M.IsBasis I C
e : α
he : e ∈ C ∧ e ∉ I
⊢ ∃ e ∈ C, I = C \ {e}

Tactic:
exact ⟨e, he.1, h.eq_of_subset_indep (hC.diff_singleton_indep he.1)
  (subset_diff_singleton h.subset he.2) diff_subset⟩

Result:
no goals

Proof state:
case refine_2.intro.intro
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
he : e ∈ C
⊢ M.IsBasis (C \ {e}) C

Tactic:
exact hC.diff_singleton_isBasis he

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I : Set α
hC : M.IsCircuit I
h : M.IsBasis I I
⊢ False

Tactic:
exact hC.dep.not_indep h.indep

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem nat_findGreatest {f : α → ℕ} {p : α → ℕ → Prop} [∀ x n, Decidable (p x n)]
    (hf : Primrec f) (hp : PrimrecRel p) : Primrec fun x => (f x).findGreatest (p x) :=
  (nat_rec' (h := fun x nih => if p x (nih.1 + 1) then nih.1 + 1 else nih.2)
    hf (const 0) (ite (hp.comp fst (snd |> fst.comp |> succ.comp))
      (snd |> fst.comp |> succ.comp) (snd.comp snd))).of_eq fun x => by
        induction f x <;> simp [Nat.findGreatest, *]

Proof state:
α : Type u_1
inst✝¹ : Primcodable α
f : α → ℕ
p : α → ℕ → Prop
inst✝ : (x : α) → (n : ℕ) → Decidable (p x n)
hf : Primrec f
hp : PrimrecRel p
x : α
⊢ Nat.rec 0 (fun n IH => if p x ((n, IH).1 + 1) then (n, IH).1 + 1 else (n, IH).2) (f x) = Nat.findGreatest (p x) (f x)

Tactic:
induction f x <;> simp [Nat.findGreatest, *]

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem cRk_union_closure_eq : M.cRk (M.closure X ∪ M.closure Y) = M.cRk (X ∪ Y)

Proof state:
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y : Set α
⊢ M.cRk (M.closure X ∪ M.closure Y) = M.cRk (X ∪ Y)

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureComp.lean
lemma integrable_compProd_snd_iff [SFinite μ] [IsSFiniteKernel κ]
    (hf : AEStronglyMeasurable f (κ ∘ₘ μ)) :
    Integrable (fun p ↦ f p.2) (μ ⊗ₘ κ) ↔ Integrable f (κ ∘ₘ μ)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
f : β → E
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
hf : AEStronglyMeasurable f (⇑κ ∘ₘ μ)
⊢ Integrable (fun p => f p.2) (μ ⊗ₘ κ) ↔ Integrable f (⇑κ ∘ₘ μ)

Tactic:
rw [← snd_compProd, Measure.snd, integrable_map_measure _ measurable_snd.aemeasurable,
  Function.comp_def]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
f : β → E
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
hf : AEStronglyMeasurable f (⇑κ ∘ₘ μ)
⊢ AEStronglyMeasurable f (map Prod.snd (μ ⊗ₘ κ))

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
f : β → E
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
hf : AEStronglyMeasurable f (⇑κ ∘ₘ μ)
⊢ AEStronglyMeasurable f (map Prod.snd (μ ⊗ₘ κ))

Tactic:
rwa [← Measure.snd, snd_compProd]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm'_eq_zero_of_ae_zero' (hq0_ne : q ≠ 0) (hμ : μ ≠ 0) {f : α → F}
    (hf_zero : f =ᵐ[μ] 0) :
    eLpNorm' f q μ = 0

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
hq0_ne : q ≠ 0
hμ : μ ≠ 0
f : α → F
hf_zero : f =ᶠ[ae μ] 0
⊢ eLpNorm' f q μ = 0

Tactic:
rw [eLpNorm'_congr_ae hf_zero, eLpNorm'_zero' hq0_ne hμ]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem le_iff_mem_closure (x y : ProjectiveSpectrum 𝒜) :
    x ≤ y ↔ y ∈ closure ({x} : Set (ProjectiveSpectrum 𝒜))

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x y : ProjectiveSpectrum 𝒜
⊢ x.asHomogeneousIdeal ≤ y.asHomogeneousIdeal ↔ ↑x.asHomogeneousIdeal ⊆ ↑y.asHomogeneousIdeal

Tactic:
simp only [as_ideal_le_as_ideal, coe_subset_coe]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x y : ProjectiveSpectrum 𝒜
⊢ x ≤ y ↔ y ∈ closure {x}

Tactic:
rw [← as_ideal_le_as_ideal, ← zeroLocus_vanishingIdeal_eq_closure, mem_zeroLocus,
  vanishingIdeal_singleton]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x y : ProjectiveSpectrum 𝒜
⊢ x.asHomogeneousIdeal ≤ y.asHomogeneousIdeal ↔ ↑x.asHomogeneousIdeal ⊆ ↑y.asHomogeneousIdeal
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem PosSemidef.fromBlocks₂₂ [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m m 𝕜)
    (B : Matrix m n 𝕜) {D : Matrix n n 𝕜} (hD : D.PosDef) [Invertible D] :
    (fromBlocks A B Bᴴ D).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef

Proof state:
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁷ : CommRing 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : D.PosDef
inst✝ : Invertible D
⊢ (fromBlocks A B Bᴴ D).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef

Tactic:
rw [← posSemidef_submatrix_equiv (Equiv.sumComm n m), Equiv.sumComm_apply,
  fromBlocks_submatrix_sum_swap_sum_swap]

Result:
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁷ : CommRing 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : D.PosDef
inst✝ : Invertible D
⊢ (fromBlocks D Bᴴ B A).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef

Proof state:
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁷ : CommRing 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : D.PosDef
inst✝ : Invertible D
⊢ (fromBlocks D Bᴴ B A).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef

Tactic:
convert PosSemidef.fromBlocks₁₁ Bᴴ A hD <;>
  simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem card_sum (α β : Type*) :
    card (α ⊕ β) = card α + card β

Proof state:
α : Type u_3
β : Type u_4
⊢ card (α ⊕ β) = card α + card β

Tactic:
simp only [card, mk_sum, map_add, toENat_lift]

Result:
no goals
-- Mathlib/Algebra/Lie/Normalizer.lean
theorem comap_normalizer (f : M' →ₗ⁅R,L⁆ M) : N.normalizer.comap f = (N.comap f).normalizer

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N : LieSubmodule R L M
f : M' →ₗ⁅R,L⁆ M
⊢ comap f N.normalizer = (comap f N).normalizer

Tactic:
ext

Result:
case h
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N : LieSubmodule R L M
f : M' →ₗ⁅R,L⁆ M
m✝ : M'
⊢ m✝ ∈ comap f N.normalizer ↔ m✝ ∈ (comap f N).normalizer

Proof state:
case h
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N : LieSubmodule R L M
f : M' →ₗ⁅R,L⁆ M
m✝ : M'
⊢ m✝ ∈ comap f N.normalizer ↔ m✝ ∈ (comap f N).normalizer

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_strict_mono {f g : α → ℝ≥0∞} (hμ : μ ≠ 0) (hg : AEMeasurable g μ)
    (hfi : ∫⁻ x, f x ∂μ ≠ ∞) (h : ∀ᵐ x ∂μ, f x < g x) : ∫⁻ x, f x ∂μ < ∫⁻ x, g x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : ¬μ univ = 0
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ

Tactic:
refine lintegral_strict_mono_of_ae_le_of_ae_lt_on hg hfi (ae_le_of_ae_lt h) hμ ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : ¬μ univ = 0
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ univ → f x < g x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : μ ≠ 0
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ

Tactic:
rw [Ne, ← Measure.measure_univ_eq_zero] at hμ

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : ¬μ univ = 0
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : ¬μ univ = 0
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ univ → f x < g x

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Data/Finset/Piecewise.lean
lemma piecewise_le_piecewise' (hf : ∀ x ∈ s, f x ≤ f' x) (hg : ∀ x ∉ s, g x ≤ g' x) :
    s.piecewise f g ≤ s.piecewise f' g' := fun x => by by_cases hx : x ∈ s <;> simp [hx, *]

Proof state:
ι : Type u_1
s : Finset ι
inst✝¹ : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g f' g' : (i : ι) → π i
inst✝ : (i : ι) → Preorder (π i)
hf : ∀ x ∈ s, f x ≤ f' x
hg : ∀ x ∉ s, g x ≤ g' x
x : ι
⊢ s.piecewise f g x ≤ s.piecewise f' g' x

Tactic:
by_cases hx : x ∈ s <;> simp [hx, *]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
@[simp]
lemma prodEquiv_symm_apply_snd (x : ToType X₁ × ToType X₂) :
    (Limits.prod.snd : X₁ ⨯ X₂ ⟶ X₂) ((prodEquiv X₁ X₂).symm x) = x.2

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ : C
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : PreservesLimit (pair X₁ X₂) (forget C)
x : ToType X₁ × ToType X₂
⊢ (ConcreteCategory.hom prod.snd) ((prodEquiv X₁ X₂).symm x) = x.2

Tactic:
obtain ⟨y, rfl⟩ := (prodEquiv X₁ X₂).surjective x

Result:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ : C
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : PreservesLimit (pair X₁ X₂) (forget C)
y : ToType (X₁ ⨯ X₂)
⊢ (ConcreteCategory.hom prod.snd) ((prodEquiv X₁ X₂).symm ((prodEquiv X₁ X₂) y)) = ((prodEquiv X₁ X₂) y).2

Proof state:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ : C
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : PreservesLimit (pair X₁ X₂) (forget C)
y : ToType (X₁ ⨯ X₂)
⊢ (ConcreteCategory.hom prod.snd) ((prodEquiv X₁ X₂).symm ((prodEquiv X₁ X₂) y)) = ((prodEquiv X₁ X₂) y).2

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem filterMap_subtype {p : α → Prop} {l : Array { x // p x }}
    {f : { x // p x } → Option β} {g : α → Option β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.filterMap f = l.unattach.filterMap g

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ filterMap f { toList := toList✝ } = filterMap g { toList := toList✝ }.unattach

Tactic:
simp only [size_toArray, List.filterMap_toArray', List.unattach_toArray, List.length_unattach,
  mk.injEq]

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ List.filterMap f toList✝ = List.filterMap g toList✝.unattach

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
l : Array { x // p x }
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ filterMap f l = filterMap g l.unattach

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ filterMap f { toList := toList✝ } = filterMap g { toList := toList✝ }.unattach

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x

Tactic:
simp [hf]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ List.filterMap f toList✝ = List.filterMap g toList✝.unattach

Tactic:
rw [List.filterMap_subtype]

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
-- Mathlib/Topology/Irreducible.lean
theorem Subtype.preirreducibleSpace (h : IsPreirreducible s) : PreirreducibleSpace s where
  isPreirreducible_univ

Proof state:
case intro.intro.intro.intro.intro.mk.intro.intro.mk.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPreirreducible s
u : Set X
hu : IsOpen u
v : Set X
hv : IsOpen v
x : X
hxs : x ∈ s
hxu : ⟨x, hxs⟩ ∈ val ⁻¹' u
y : X
hys : y ∈ s
hyv : ⟨y, hys⟩ ∈ val ⁻¹' v
⊢ (univ ∩ (val ⁻¹' u ∩ val ⁻¹' v)).Nonempty

Tactic:
rcases h u v hu hv ⟨x, hxs, hxu⟩ ⟨y, hys, hyv⟩ with ⟨x, hxs, ⟨hxu, hxv⟩⟩

Result:
case intro.intro.intro.intro.intro.mk.intro.intro.mk.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPreirreducible s
u : Set X
hu : IsOpen u
v : Set X
hv : IsOpen v
x✝ : X
hxs✝ : x✝ ∈ s
hxu✝ : ⟨x✝, hxs✝⟩ ∈ val ⁻¹' u
y : X
hys : y ∈ s
hyv : ⟨y, hys⟩ ∈ val ⁻¹' v
x : X
hxs : x ∈ s
hxu : x ∈ u
hxv : x ∈ v
⊢ (univ ∩ (val ⁻¹' u ∩ val ⁻¹' v)).Nonempty

Proof state:
case intro.intro.intro.intro.intro.mk.intro.intro.mk.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPreirreducible s
u : Set X
hu : IsOpen u
v : Set X
hv : IsOpen v
x✝ : X
hxs✝ : x✝ ∈ s
hxu✝ : ⟨x✝, hxs✝⟩ ∈ val ⁻¹' u
y : X
hys : y ∈ s
hyv : ⟨y, hys⟩ ∈ val ⁻¹' v
x : X
hxs : x ∈ s
hxu : x ∈ u
hxv : x ∈ v
⊢ (univ ∩ (val ⁻¹' u ∩ val ⁻¹' v)).Nonempty

Tactic:
exact ⟨⟨x, hxs⟩, ⟨Set.mem_univ _, ⟨hxu, hxv⟩⟩⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPreirreducible s
⊢ IsPreirreducible univ

Tactic:
rintro _ _ ⟨u, hu, rfl⟩ ⟨v, hv, rfl⟩ ⟨⟨x, hxs⟩, -, hxu⟩ ⟨⟨y, hys⟩, -, hyv⟩

Result:
case intro.intro.intro.intro.intro.mk.intro.intro.mk.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPreirreducible s
u : Set X
hu : IsOpen u
v : Set X
hv : IsOpen v
x : X
hxs : x ∈ s
hxu : ⟨x, hxs⟩ ∈ val ⁻¹' u
y : X
hys : y ∈ s
hyv : ⟨y, hys⟩ ∈ val ⁻¹' v
⊢ (univ ∩ (val ⁻¹' u ∩ val ⁻¹' v)).Nonempty
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integral_indicator_const [CompleteSpace E] (e : E) ⦃s : Set X⦄ (s_meas : MeasurableSet s) :
    ∫ x : X, s.indicator (fun _ : X => e) x ∂μ = (μ s).toReal • e

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure X
inst✝ : CompleteSpace E
e : E
s : Set X
s_meas : MeasurableSet s
⊢ ∫ (x : X), s.indicator (fun x => e) x ∂μ = (μ s).toReal • e

Tactic:
rw [integral_indicator s_meas, ← setIntegral_const]

Result:
no goals
-- Mathlib/RingTheory/Derivation/MapCoeffs.lean
@[simp]
lemma mapCoeffs_C (x : A) :
    mapCoeffs (C x) = C x′

Proof state:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Differential A
x : A
⊢ mapCoeffs (C x) = C x′

Tactic:
simp [← monomial_zero_left]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
theorem inj_right (hm : IsHomogeneous φ m) (hn : IsHomogeneous φ n) (hφ : φ ≠ 0) : m = n

Proof state:
case intro
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m n : ℕ
hm : φ.IsHomogeneous m
hn : φ.IsHomogeneous n
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ m = n

Tactic:
rw [← hm hd, ← hn hd]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m n : ℕ
hm : φ.IsHomogeneous m
hn : φ.IsHomogeneous n
hφ : φ ≠ 0
⊢ m = n

Tactic:
obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero hφ

Result:
case intro
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m n : ℕ
hm : φ.IsHomogeneous m
hn : φ.IsHomogeneous n
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ m = n
-- Mathlib/Algebra/Group/Fin/Basic.lean
lemma add_lt_left_iff {n : ℕ} {a b : Fin n} : a + b < a ↔ rev b < a

Proof state:
n : ℕ
a b : Fin n
⊢ a + b < a ↔ b.rev < a

Tactic:
rw [← rev_lt_rev, Iff.comm, ← rev_lt_rev, rev_add, lt_sub_iff, rev_rev]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma homologyIsoSc'_inv_ι :
    (K.homologyIsoSc' i j k hi hk).inv ≫ K.homologyι j =
      (K.sc' i j k).homologyι ≫ (K.opcyclesIsoSc' i j k hi hk).inv

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.homologyIsoSc' i j k hi hk).inv ≫ K.homologyι j = (K.sc' i j k).homologyι ≫ (K.opcyclesIsoSc' i j k hi hk).inv

Tactic:
apply ShortComplex.homologyι_naturality

Result:
no goals