harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
lemma quot_mk_eq_iff [Mono f] (a b : X₁ ⊕ X₂) :
    (Quot.mk _ a : Pushout f g) = Quot.mk _ b ↔ Rel' f g a b

Proof state:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
a b : X₁ ⊕ X₂
⊢ Quot.mk (Rel f g) a = Quot.mk (Rel f g) b ↔ Rel' f g a b

Tactic:
rw [← (equivalence_rel' f g).quot_mk_eq_iff]

Result:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
a b : X₁ ⊕ X₂
⊢ Quot.mk (Rel f g) a = Quot.mk (Rel f g) b ↔ Quot.mk (Rel' f g) a = Quot.mk (Rel' f g) b

Proof state:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
a b : X₁ ⊕ X₂
⊢ Quot.mk (Rel f g) a = Quot.mk (Rel f g) b ↔ Quot.mk (Rel' f g) a = Quot.mk (Rel' f g) b

Tactic:
exact ⟨fun h => (equivPushout' f g).symm.injective h,
  fun h => (equivPushout' f g).injective h⟩

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean
theorem smul_balancedCore_subset (s : Set E) {a : 𝕜} (ha : ‖a‖ ≤ 1) :
    a • balancedCore 𝕜 s ⊆ balancedCore 𝕜 s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • balancedCore 𝕜 s ⊆ balancedCore 𝕜 s

Tactic:
rintro x ⟨y, hy, rfl⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : y ∈ balancedCore 𝕜 s
⊢ (fun x => a • x) y ∈ balancedCore 𝕜 s

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
t : Set E
ht1 : Balanced 𝕜 t
ht2 : t ⊆ s
hy : y ∈ t
⊢ (fun x => a • x) y ∈ balancedCore 𝕜 s

Tactic:
exact ⟨t, ⟨ht1, ht2⟩, ht1 a ha (smul_mem_smul_set hy)⟩

Result:
no goals

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : y ∈ balancedCore 𝕜 s
⊢ (fun x => a • x) y ∈ balancedCore 𝕜 s

Tactic:
rw [mem_balancedCore_iff] at hy

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ y ∈ t
⊢ (fun x => a • x) y ∈ balancedCore 𝕜 s

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ y ∈ t
⊢ (fun x => a • x) y ∈ balancedCore 𝕜 s

Tactic:
rcases hy with ⟨t, ht1, ht2, hy⟩

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
t : Set E
ht1 : Balanced 𝕜 t
ht2 : t ⊆ s
hy : y ∈ t
⊢ (fun x => a • x) y ∈ balancedCore 𝕜 s
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem cpow_eq_nhds' {p : ℂ × ℂ} (hp_fst : p.fst ≠ 0) :
    (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2)

Proof state:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
this : ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.1 ≠ 0
x : ℂ × ℂ
hx : x.1 ≠ 0
⊢ x.1 ^ x.2 = cexp (Complex.log x.1 * x.2)

Tactic:
rw [cpow_def_of_ne_zero hx]

Result:
no goals

Proof state:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
⊢ IsOpen {x | x.1 = 0}ᶜ

Tactic:
rw [isOpen_compl_iff]

Result:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
⊢ IsClosed {x | x.1 = 0}

Proof state:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.1 ≠ 0

Tactic:
refine IsOpen.eventually_mem ?_ hp_fst

Result:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
⊢ IsOpen fun x => x.1 = 0 → False

Proof state:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
this : ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.1 ≠ 0
x : ℂ × ℂ
hx : x.1 ≠ 0
⊢ (fun x => x.1 ^ x.2) x = (fun x => cexp (Complex.log x.1 * x.2)) x

Tactic:
dsimp only

Result:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
this : ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.1 ≠ 0
x : ℂ × ℂ
hx : x.1 ≠ 0
⊢ x.1 ^ x.2 = cexp (Complex.log x.1 * x.2)

Proof state:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
⊢ IsClosed {x | x.1 = 0}

Tactic:
exact isClosed_eq continuous_fst continuous_const

Result:
no goals

Proof state:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
⊢ IsOpen fun x => x.1 = 0 → False

Tactic:
change IsOpen { x : ℂ × ℂ | x.1 = 0 }ᶜ

Result:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
⊢ IsOpen {x | x.1 = 0}ᶜ

Proof state:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
⊢ (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => cexp (Complex.log x.1 * x.2)

Tactic:
suffices ∀ᶠ x : ℂ × ℂ in 𝓝 p, x.1 ≠ 0 from
  this.mono fun x hx ↦ by
    dsimp only
    rw [cpow_def_of_ne_zero hx]

Result:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.1 ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
    get? (m.erase k) k = none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
⊢ get? (m.erase k) k = none

Tactic:
simp_to_model [erase] using List.getValue?_eraseKey_self

Result:
no goals
-- Mathlib/Probability/Martingale/BorelCantelli.lean
theorem martingalePart_process_ae_eq (ℱ : Filtration ℕ m0) (μ : Measure Ω) (s : ℕ → Set Ω) (n : ℕ) :
    martingalePart (process s) ℱ μ n =
      ∑ k ∈ Finset.range n, ((s (k + 1)).indicator 1 - μ[(s (k + 1)).indicator 1|ℱ k])

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
⊢ martingalePart (process s) ℱ μ n = ∑ k ∈ Finset.range n, ((s (k + 1)).indicator 1 - μ[(s (k + 1)).indicator 1|↑ℱ k])

Tactic:
simp only [martingalePart_eq_sum, process_zero, zero_add]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
⊢ ∑ i ∈ Finset.range n, (process s (i + 1) - process s i - μ[process s (i + 1) - process s i|↑ℱ i]) =
    ∑ k ∈ Finset.range n, ((s (k + 1)).indicator 1 - μ[(s (k + 1)).indicator 1|↑ℱ k])

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n k : ℕ
x✝ : k ∈ Finset.range n
⊢ process s (k + 1) - process s k - μ[process s (k + 1) - process s k|↑ℱ k] =
    (s (k + 1)).indicator 1 - μ[(s (k + 1)).indicator 1|↑ℱ k]

Tactic:
simp only [process, Finset.sum_range_succ_sub_sum]

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
⊢ ∑ i ∈ Finset.range n, (process s (i + 1) - process s i - μ[process s (i + 1) - process s i|↑ℱ i]) =
    ∑ k ∈ Finset.range n, ((s (k + 1)).indicator 1 - μ[(s (k + 1)).indicator 1|↑ℱ k])

Tactic:
refine Finset.sum_congr rfl fun k _ => ?_

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n k : ℕ
x✝ : k ∈ Finset.range n
⊢ process s (k + 1) - process s k - μ[process s (k + 1) - process s k|↑ℱ k] =
    (s (k + 1)).indicator 1 - μ[(s (k + 1)).indicator 1|↑ℱ k]
-- Mathlib/Order/Compare.lean
theorem lt_iff_lt_of_cmp_eq_cmp (h : cmp x y = cmp x' y') : x < y ↔ x' < y'

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x < y ↔ x' < y'

Tactic:
rw [← cmp_eq_lt_iff, ← cmp_eq_lt_iff, h]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthSup_iSup {ι : Type*} [Finite ι] (u : ι → ℕ → ℝ≥0∞) :
    expGrowthSup (⨆ i, u i) = ⨆ i, expGrowthSup (u i)

Proof state:
ι : Type u_1
inst✝ : Finite ι
u : ι → ℕ → ℝ≥0∞
⊢ expGrowthSup (⨆ i, u i) = ⨆ i, expGrowthSup (u i)

Tactic:
rw [← iSup_univ, expGrowthSup_biSup u Set.finite_univ, iSup_univ]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
theorem sum_Ico_Ico_comm' {M : Type*} [AddCommMonoid M] (a b : ℕ) (f : ℕ → ℕ → M) :
    (∑ i ∈ Finset.Ico a b, ∑ j ∈ Finset.Ico (i + 1) b, f i j) =
      ∑ j ∈ Finset.Ico a b, ∑ i ∈ Finset.Ico a j, f i j

Proof state:
M : Type u_3
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ i ∈ Ico a b, ∑ j ∈ Ico (i + 1) b, f i j = ∑ j ∈ Ico a b, ∑ i ∈ Ico a j, f i j

Tactic:
rw [Finset.sum_sigma', Finset.sum_sigma']

Result:
M : Type u_3
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ x ∈ (Ico a b).sigma fun i => Ico (i + 1) b, f x.fst x.snd = ∑ x ∈ (Ico a b).sigma (Ico a), f x.snd x.fst

Proof state:
M : Type u_3
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ x ∈ (Ico a b).sigma fun i => Ico (i + 1) b, f x.fst x.snd = ∑ x ∈ (Ico a b).sigma (Ico a), f x.snd x.fst

Tactic:
refine sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) ?_ ?_ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
  (fun _ _ ↦ rfl) <;>
simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma] <;>
rintro a b ⟨⟨h₁, h₂⟩, ⟨h₃, h₄⟩⟩ <;>
omega

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem nonunits_le_nonunits {A B : ValuationSubring K} : B.nonunits ≤ A.nonunits ↔ A ≤ B

Proof state:
K : Type u
inst✝ : Field K
A B : ValuationSubring K
⊢ B.nonunits ≤ A.nonunits ↔ A ≤ B

Tactic:
constructor

Result:
case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
⊢ B.nonunits ≤ A.nonunits → A ≤ B

case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
⊢ A ≤ B → B.nonunits ≤ A.nonunits

Proof state:
case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : x ∈ A
⊢ x ∈ B

Tactic:
by_cases h_1 : x = 0

Result:
case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : x ∈ A
h_1 : x = 0
⊢ x ∈ B

case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : x ∈ A
h_1 : ¬x = 0
⊢ x ∈ B

Proof state:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
⊢ A ≤ B → B.nonunits ≤ A.nonunits

Tactic:
intro h x hx

Result:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : K
hx : x ∈ B.nonunits
⊢ x ∈ A.nonunits

Proof state:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : K
hx : x ∈ B.nonunits
h_1 : x ∉ A.nonunits
⊢ False

Tactic:
exact not_lt.2 (monotone_mapOfLE _ _ h (not_lt.1 h_1)) hx

Result:
no goals

Proof state:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : K
hx : x ∈ B.nonunits
⊢ x ∈ A.nonunits

Tactic:
by_contra h_1

Result:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : K
hx : x ∈ B.nonunits
h_1 : x ∉ A.nonunits
⊢ False

Proof state:
case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
⊢ B.nonunits ≤ A.nonunits → A ≤ B

Tactic:
intro h x hx

Result:
case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : x ∈ A
⊢ x ∈ B

Proof state:
case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : x ∈ A
h_1 : x = 0
⊢ x ∈ B

Tactic:
simp only [h_1, zero_mem]

Result:
no goals

Proof state:
case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : ¬A.valuation x⁻¹ < 1
h_1 : ¬x = 0
⊢ ¬B.valuation x⁻¹ < 1

Tactic:
by_contra h_2

Result:
case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : ¬A.valuation x⁻¹ < 1
h_1 : ¬x = 0
h_2 : B.valuation x⁻¹ < 1
⊢ False

Proof state:
case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : ¬A.valuation x⁻¹ < 1
h_1 : ¬x = 0
h_2 : B.valuation x⁻¹ < 1
⊢ False

Tactic:
exact hx (h h_2)

Result:
no goals

Proof state:
case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : x ∈ A
h_1 : ¬x = 0
⊢ x ∈ B

Tactic:
rw [← valuation_le_one_iff, ← not_lt, Valuation.one_lt_val_iff _ h_1] at hx ⊢

Result:
case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : ¬A.valuation x⁻¹ < 1
h_1 : ¬x = 0
⊢ ¬B.valuation x⁻¹ < 1
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem UniformContinuousOn.continuousOn [UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α}
    (h : UniformContinuousOn f s) : ContinuousOn f s

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : UniformContinuousOn f s
⊢ ContinuousOn f s

Tactic:
rw [uniformContinuousOn_iff_restrict] at h

Result:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : UniformContinuous (s.restrict f)
⊢ ContinuousOn f s

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : UniformContinuous (s.restrict f)
⊢ Continuous (s.restrict f)

Tactic:
exact h.continuous

Result:
no goals

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : UniformContinuous (s.restrict f)
⊢ ContinuousOn f s

Tactic:
rw [continuousOn_iff_continuous_restrict]

Result:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : UniformContinuous (s.restrict f)
⊢ Continuous (s.restrict f)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Core.lean
theorem Relation.TransGen.trans {α : Sort u} {r : α → α → Prop} {a b c} :
    TransGen r a b → TransGen r b c → TransGen r a c

Proof state:
case tail
α : Sort u
r : α → α → Prop
a b c : α
hab : TransGen r a b
b✝ c✝ : α
a✝ : TransGen r b b✝
h : r b✝ c✝
ih : TransGen r a b✝
⊢ TransGen r a c✝

Tactic:
exact TransGen.tail ih h

Result:
no goals

Proof state:
α : Sort u
r : α → α → Prop
a b c : α
⊢ TransGen r a b → TransGen r b c → TransGen r a c

Tactic:
intro hab hbc

Result:
α : Sort u
r : α → α → Prop
a b c : α
hab : TransGen r a b
hbc : TransGen r b c
⊢ TransGen r a c

Proof state:
case single
α : Sort u
r : α → α → Prop
a b c : α
hab : TransGen r a b
b✝ : α
h : r b b✝
⊢ TransGen r a b✝

Tactic:
exact TransGen.tail hab h

Result:
no goals

Proof state:
α : Sort u
r : α → α → Prop
a b c : α
hab : TransGen r a b
hbc : TransGen r b c
⊢ TransGen r a c

Tactic:
induction hbc with
| single h => exact TransGen.tail hab h
| tail _ h ih => exact TransGen.tail ih h

Result:
no goals
-- Mathlib/Data/Nat/Squarefree.lean
theorem squarefree_of_factorization_le_one {n : ℕ} (hn : n ≠ 0) (hn' : ∀ p, n.factorization p ≤ 1) :
    Squarefree n

Proof state:
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), n.factorization p ≤ 1
a : ℕ
⊢ List.count a n.primeFactorsList ≤ 1

Tactic:
rw [primeFactorsList_count_eq]

Result:
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), n.factorization p ≤ 1
a : ℕ
⊢ n.factorization a ≤ 1

Proof state:
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), n.factorization p ≤ 1
⊢ Squarefree n

Tactic:
rw [squarefree_iff_nodup_primeFactorsList hn, List.nodup_iff_count_le_one]

Result:
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), n.factorization p ≤ 1
⊢ ∀ (a : ℕ), List.count a n.primeFactorsList ≤ 1

Proof state:
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), n.factorization p ≤ 1
⊢ ∀ (a : ℕ), List.count a n.primeFactorsList ≤ 1

Tactic:
intro a

Result:
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), n.factorization p ≤ 1
a : ℕ
⊢ List.count a n.primeFactorsList ≤ 1

Proof state:
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), n.factorization p ≤ 1
a : ℕ
⊢ n.factorization a ≤ 1

Tactic:
apply hn'

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem bind₂_monomial_one (f : R →+* MvPolynomial σ S) (d : σ →₀ ℕ) :
    bind₂ f (monomial d 1) = monomial d 1

Proof state:
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* MvPolynomial σ S
d : σ →₀ ℕ
⊢ (bind₂ f) ((monomial d) 1) = (monomial d) 1

Tactic:
rw [bind₂_monomial, f.map_one, one_mul]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degreeOf_mul_le (i : σ) (f g : MvPolynomial σ R) :
    degreeOf i (f * g) ≤ degreeOf i f + degreeOf i g

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ degreeOf i (f * g) ≤ degreeOf i f + degreeOf i g

Tactic:
classical
simp only [degreeOf]
convert Multiset.count_le_of_le i degrees_mul_le
rw [Multiset.count_add]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ degreeOf i (f * g) ≤ degreeOf i f + degreeOf i g

Tactic:
simp only [degreeOf]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i (f * g).degrees ≤ Multiset.count i f.degrees + Multiset.count i g.degrees

Proof state:
case h.e'_4
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i f.degrees + Multiset.count i g.degrees = Multiset.count i (f.degrees + g.degrees)

Tactic:
rw [Multiset.count_add]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i (f * g).degrees ≤ Multiset.count i f.degrees + Multiset.count i g.degrees

Tactic:
convert Multiset.count_le_of_le i degrees_mul_le

Result:
case h.e'_4
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i f.degrees + Multiset.count i g.degrees = Multiset.count i (f.degrees + g.degrees)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem getElem?_zero_filter (p : α → Bool) (l : Vector α n) :
    (l.filter p)[0]? = l.find? p

Proof state:
α : Type
n : Nat
p : α → Bool
l : Vector α n
⊢ (Array.filter p l.toArray)[0]? = find? p l

Tactic:
cases l

Result:
case mk
α : Type
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (Array.filter p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray)[0]? =
    find? p { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (Array.filter p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray)[0]? =
    find? p { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp [← List.head?_eq_getElem?]

Result:
no goals
-- Mathlib/Tactic/CancelDenoms/Core.lean
theorem add_subst {α} [Ring α] {n e1 e2 t1 t2 : α} (h1 : n * e1 = t1) (h2 : n * e2 = t2) :
    n * (e1 + e2) = t1 + t2

Proof state:
α : Type u_1
inst✝ : Ring α
n e1 e2 t1 t2 : α
h1 : n * e1 = t1
h2 : n * e2 = t2
⊢ n * (e1 + e2) = t1 + t2

Tactic:
simp [left_distrib, *]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Basic.lean
theorem lift_comp : (hf.lift g h).comp f = g

Proof state:
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap ⇑f
g : C(X, Z)
h : FactorsThrough ⇑g ⇑f
a✝ : X
⊢ ((hf.lift g h).comp f) a✝ = g a✝

Tactic:
simpa using h (Function.rightInverse_surjInv _ _)

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap ⇑f
g : C(X, Z)
h : FactorsThrough ⇑g ⇑f
⊢ (hf.lift g h).comp f = g

Tactic:
ext

Result:
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap ⇑f
g : C(X, Z)
h : FactorsThrough ⇑g ⇑f
a✝ : X
⊢ ((hf.lift g h).comp f) a✝ = g a✝
-- Mathlib/CategoryTheory/Subobject/FactorThru.lean
theorem factors_congr {X : C} {f g : MonoOver X} {Y : C} (h : Y ⟶ X) (e : f ≅ g) :
    f.Factors h ↔ g.Factors h :=
  ⟨fun ⟨u, hu⟩ => ⟨u ≫ ((MonoOver.forget _).map e.hom).left, by simp [hu]⟩, fun ⟨u, hu⟩ =>
    ⟨u ≫ ((MonoOver.forget _).map e.inv).left, by simp [hu]⟩⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
f g : MonoOver X
Y : C
h : Y ⟶ X
e : f ≅ g
x✝ : g.Factors h
u : Y ⟶ g.obj.left
hu : u ≫ g.arrow = h
⊢ (u ≫ ((forget X).map e.inv).left) ≫ f.arrow = h

Tactic:
simp [hu]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
f g : MonoOver X
Y : C
h : Y ⟶ X
e : f ≅ g
x✝ : f.Factors h
u : Y ⟶ f.obj.left
hu : u ≫ f.arrow = h
⊢ (u ≫ ((forget X).map e.hom).left) ≫ g.arrow = h

Tactic:
simp [hu]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem smul_inf [SMul R ℝ] [SMul R ℝ≥0] [IsScalarTower R ℝ≥0 ℝ] (r : R) (p q : Seminorm 𝕜 E) :
    r • (p ⊓ q) = r • p ⊓ r • q

Proof state:
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
⊢ r • (p ⊓ q) = r • p ⊓ r • q

Tactic:
ext

Result:
case h
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x✝ : E
⊢ (r • (p ⊓ q)) x✝ = (r • p ⊓ r • q) x✝

Proof state:
case h
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x✝ : E
⊢ (r • (p ⊓ q)) x✝ = (r • p ⊓ r • q) x✝

Tactic:
simp_rw [smul_apply, inf_apply, smul_apply, ← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def,
  smul_eq_mul, Real.mul_iInf_of_nonneg (NNReal.coe_nonneg _), mul_add]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem ordProj_dvd_ordProj_of_dvd {a b : ℕ} (hb0 : b ≠ 0) (hab : a ∣ b) (p : ℕ) :
    ordProj[p] a ∣ ordProj[p] b

Proof state:
case inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

Tactic:
rcases eq_or_ne a 0 with (rfl | ha0)

Result:
case inr.inl
b : ℕ
hb0 : b ≠ 0
p : ℕ
pp : Prime p
hab : 0 ∣ b
⊢ p ^ (factorization 0) p ∣ p ^ b.factorization p

case inr.inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

Proof state:
case inr.inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ a.factorization p ≤ b.factorization p

Tactic:
exact (factorization_le_iff_dvd ha0 hb0).2 hab p

Result:
no goals

Proof state:
case inr.inl
b : ℕ
hb0 : b ≠ 0
p : ℕ
pp : Prime p
hab : 0 ∣ b
⊢ p ^ (factorization 0) p ∣ p ^ b.factorization p

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

Tactic:
rw [pow_dvd_pow_iff_le_right pp.one_lt]

Result:
case inr.inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ a.factorization p ≤ b.factorization p

Proof state:
case inl
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

Tactic:
simp [pp]

Result:
no goals

Proof state:
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

Tactic:
rcases em' p.Prime with (pp | pp)

Result:
case inl
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

case inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ p ^ a.factorization p ∣ p ^ b.factorization p
-- Mathlib/Probability/Integration.lean
theorem IndepFun.integrable_left_of_integrable_mul {β : Type*} [MeasurableSpace β] {X Y : Ω → β}
    [NormedDivisionRing β] [BorelSpace β] (hXY : IndepFun X Y μ) (h'XY : Integrable (X * Y) μ)
    (hX : AEStronglyMeasurable X μ) (hY : AEStronglyMeasurable Y μ) (h'Y : ¬Y =ᵐ[μ] 0) :
    Integrable X μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖X a‖ₑ ∂μ = ⊤
J : IndepFun (fun x => ‖X x‖ₑ) (fun x => ‖Y x‖ₑ) μ
A : ∫⁻ (ω : Ω), ‖X ω * Y ω‖ₑ ∂μ < ⊤
⊢ False

Tactic:
simp only [enorm_mul, ENNReal.coe_mul] at A

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖X a‖ₑ ∂μ = ⊤
J : IndepFun (fun x => ‖X x‖ₑ) (fun x => ‖Y x‖ₑ) μ
A : ∫⁻ (ω : Ω), ‖X ω‖ₑ * ‖Y ω‖ₑ ∂μ < ⊤
⊢ False