harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem mul_prod_erase (f : α →₀ M) (y : α) (g : α → M → N) (hyf : y ∈ f.support) :
    g y (f y) * (erase y f).prod g = f.prod g

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
⊢ g y (f y) * (erase y f).prod g = f.prod g

Tactic:
rw [Finsupp.prod, Finsupp.prod, ← Finset.mul_prod_erase _ _ hyf, Finsupp.support_erase,
  Finset.prod_congr rfl]

Result:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
⊢ ∀ x ∈ f.support.erase y, g x ((erase y f) x) = g x (f x)

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
h : α
hx : h ∈ f.support.erase y
⊢ g h ((erase y f) h) = g h (f h)

Tactic:
rw [Finsupp.erase_ne (ne_of_mem_erase hx)]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
⊢ ∀ x ∈ f.support.erase y, g x ((erase y f) x) = g x (f x)

Tactic:
intro h hx

Result:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
h : α
hx : h ∈ f.support.erase y
⊢ g h ((erase y f) h) = g h (f h)

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
⊢ g y (f y) * (erase y f).prod g = f.prod g

Tactic:
classical
  rw [Finsupp.prod, Finsupp.prod, ← Finset.mul_prod_erase _ _ hyf, Finsupp.support_erase,
    Finset.prod_congr rfl]
  intro h hx
  rw [Finsupp.erase_ne (ne_of_mem_erase hx)]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem minFac_two : minFac 2 = 2

Proof state:
⊢ minFac 2 = 2

Tactic:
simp [minFac, minFacAux]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem adjoin_simple_isCompactElement (x : E) : IsCompactElement F⟮x⟯

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
s : Set (IntermediateField F E)
hne : s.Nonempty
hs : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hx : x ∈ ⨆ a, ↑a
this : Nonempty ↑s
⊢ ∃ x_1, ∃ (_ : x_1 ∈ s), x ∈ x_1

Tactic:
rwa [← SetLike.mem_coe, coe_iSup_of_directed hs.directed_val, mem_iUnion, Subtype.exists] at hx

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
⊢ IsCompactElement F⟮x⟯

Tactic:
simp_rw [isCompactElement_iff_le_of_directed_sSup_le,
  adjoin_simple_le_iff, sSup_eq_iSup', ← exists_prop]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
⊢ ∀ (s : Set (IntermediateField F E)),
    s.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) s → x ∈ ⨆ a, ↑a → ∃ x_1, ∃ (_ : x_1 ∈ s), x ∈ x_1

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
⊢ ∀ (s : Set (IntermediateField F E)),
    s.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) s → x ∈ ⨆ a, ↑a → ∃ x_1, ∃ (_ : x_1 ∈ s), x ∈ x_1

Tactic:
intro s hne hs hx

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
s : Set (IntermediateField F E)
hne : s.Nonempty
hs : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hx : x ∈ ⨆ a, ↑a
⊢ ∃ x_1, ∃ (_ : x_1 ∈ s), x ∈ x_1

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
s : Set (IntermediateField F E)
hne : s.Nonempty
hs : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hx : x ∈ ⨆ a, ↑a
⊢ ∃ x_1, ∃ (_ : x_1 ∈ s), x ∈ x_1

Tactic:
have := hne.to_subtype

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
s : Set (IntermediateField F E)
hne : s.Nonempty
hs : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hx : x ∈ ⨆ a, ↑a
this : Nonempty ↑s
⊢ ∃ x_1, ∃ (_ : x_1 ∈ s), x ∈ x_1
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem prod {f : α → β} {Kf : ℝ≥0} (hf : LipschitzWith Kf f) {g : α → γ} {Kg : ℝ≥0}
    (hg : LipschitzWith Kg g) : LipschitzWith (max Kf Kg) fun x => (f x, g x)

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
⊢ LipschitzWith (Kf ⊔ Kg) fun x => (f x, g x)

Tactic:
intro x y

Result:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
x y : α
⊢ edist ((fun x => (f x, g x)) x) ((fun x => (f x, g x)) y) ≤ ↑(Kf ⊔ Kg) * edist x y

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
x y : α
⊢ edist ((fun x => (f x, g x)) x).1 ((fun x => (f x, g x)) y).1 ⊔
      edist ((fun x => (f x, g x)) x).2 ((fun x => (f x, g x)) y).2 ≤
    ↑Kf * edist x y ⊔ ↑Kg * edist x y

Tactic:
exact max_le_max (hf x y) (hg x y)

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
x y : α
⊢ edist ((fun x => (f x, g x)) x) ((fun x => (f x, g x)) y) ≤ ↑(Kf ⊔ Kg) * edist x y

Tactic:
rw [ENNReal.coe_mono.map_max, Prod.edist_eq, max_mul]

Result:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
x y : α
⊢ edist ((fun x => (f x, g x)) x).1 ((fun x => (f x, g x)) y).1 ⊔
      edist ((fun x => (f x, g x)) x).2 ((fun x => (f x, g x)) y).2 ≤
    ↑Kf * edist x y ⊔ ↑Kg * edist x y
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_le_rpow_of_exponent_le {x : ℝ≥0∞} {y z : ℝ} (hx : 1 ≤ x) (hyz : y ≤ z) :
    x ^ y ≤ x ^ z

Proof state:
x : ℝ≥0∞
y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ x ^ y ≤ x ^ z

Tactic:
cases x

Result:
case top
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ⊤
⊢ ⊤ ^ y ≤ ⊤ ^ z

case coe
y z : ℝ
hyz : y ≤ z
x✝ : ℝ≥0
hx : 1 ≤ ↑x✝
⊢ ↑x✝ ^ y ≤ ↑x✝ ^ z

Proof state:
case coe
y z : ℝ
hyz : y ≤ z
x✝ : ℝ≥0
hx : 1 ≤ ↑x✝
⊢ ↑x✝ ^ y ≤ ↑x✝ ^ z

Tactic:
simp only [one_le_coe_iff, some_eq_coe] at hx

Result:
case coe
y z : ℝ
hyz : y ≤ z
x✝ : ℝ≥0
hx : 1 ≤ x✝
⊢ ↑x✝ ^ y ≤ ↑x✝ ^ z

Proof state:
case coe
y z : ℝ
hyz : y ≤ z
x✝ : ℝ≥0
hx : 1 ≤ x✝
⊢ ↑x✝ ^ y ≤ ↑x✝ ^ z

Tactic:
simp [← coe_rpow_of_ne_zero (ne_of_gt (lt_of_lt_of_le zero_lt_one hx)),
  NNReal.rpow_le_rpow_of_exponent_le hx hyz]

Result:
no goals

Proof state:
case top
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ⊤
⊢ ⊤ ^ y ≤ ⊤ ^ z

Tactic:
rcases lt_trichotomy y 0 with (Hy | Hy | Hy) <;>
rcases lt_trichotomy z 0 with (Hz | Hz | Hz) <;>
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos, le_refl] <;>
linarith

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem eq_div_iff (ha : a ≠ 0) (ha' : a ≠ ∞) : b = c / a ↔ a * b = c :=
  ⟨fun h => by rw [h, ENNReal.mul_div_cancel ha ha'], fun h => by
    rw [← h, mul_div_assoc, ENNReal.mul_div_cancel ha ha']⟩

Proof state:
a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : b = c / a
⊢ a * b = c

Tactic:
rw [h, ENNReal.mul_div_cancel ha ha']

Result:
no goals

Proof state:
a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a * b = c
⊢ b = c / a

Tactic:
rw [← h, mul_div_assoc, ENNReal.mul_div_cancel ha ha']

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
lemma pow_pos_iff (hn : n ≠ 0) : 0 < a ^ n ↔ 0 < a

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedCommMonoidWithZero α
a : α
n : ℕ
inst✝ : NoZeroDivisors α
hn : n ≠ 0
⊢ 0 < a ^ n ↔ 0 < a

Tactic:
simp_rw [zero_lt_iff, pow_ne_zero_iff hn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx_le_length (p : α → Bool) {xs : List α} : xs.findIdx p ≤ xs.length

Proof state:
case neg
α : Type u_1
p : α → Bool
xs : List α
e : ¬∃ x, x ∈ xs ∧ p x = true
⊢ findIdx p xs ≤ xs.length

Tactic:
simp at e

Result:
case neg
α : Type u_1
p : α → Bool
xs : List α
e : ∀ (x : α), x ∈ xs → p x = false
⊢ findIdx p xs ≤ xs.length

Proof state:
α : Type u_1
p : α → Bool
xs : List α
⊢ findIdx p xs ≤ xs.length

Tactic:
by_cases e : ∃ x ∈ xs, p x

Result:
case pos
α : Type u_1
p : α → Bool
xs : List α
e : ∃ x, x ∈ xs ∧ p x = true
⊢ findIdx p xs ≤ xs.length

case neg
α : Type u_1
p : α → Bool
xs : List α
e : ¬∃ x, x ∈ xs ∧ p x = true
⊢ findIdx p xs ≤ xs.length

Proof state:
case pos
α : Type u_1
p : α → Bool
xs : List α
e : ∃ x, x ∈ xs ∧ p x = true
⊢ findIdx p xs ≤ xs.length

Tactic:
exact Nat.le_of_lt (findIdx_lt_length_of_exists e)

Result:
no goals

Proof state:
case neg
α : Type u_1
p : α → Bool
xs : List α
e : ∀ (x : α), x ∈ xs → p x = false
⊢ findIdx p xs ≤ xs.length

Tactic:
exact Nat.le_of_eq (findIdx_eq_length.mpr e)

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toReal_mul_top (a : ℝ≥0∞) : ENNReal.toReal (a * ∞) = 0

Proof state:
a : ℝ≥0∞
⊢ (a * ⊤).toReal = 0

Tactic:
rw [toReal_mul, top_toReal, mul_zero]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem leadingCoeff_pow_X_add_C (r : R) (i : ℕ) : leadingCoeff ((X + C r) ^ i) = 1

Proof state:
R : Type u
inst✝ : Semiring R
r : R
i : ℕ
⊢ ((X + C r) ^ i).leadingCoeff = 1

Tactic:
nontriviality

Result:
R : Type u
inst✝ : Semiring R
r : R
i : ℕ
a✝ : Nontrivial R
⊢ ((X + C r) ^ i).leadingCoeff = 1

Proof state:
R : Type u
inst✝ : Semiring R
r : R
i : ℕ
a✝ : Nontrivial R
⊢ ((X + C r) ^ i).leadingCoeff = 1

Tactic:
rw [leadingCoeff_pow'] <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem norm_eq_integral (f : α →₁ₛ[μ] E) : ‖f‖ = ((toSimpleFunc f).map norm).integral μ

Proof state:
α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc E 1 μ)
⊢ ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖ =
    ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal • ‖x‖

Tactic:
simp_rw [smul_eq_mul]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc E 1 μ)
⊢ ‖f‖ = SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc f))

Tactic:
rw [norm_eq_sum_mul f, (toSimpleFunc f).map_integral norm (SimpleFunc.integrable f) norm_zero]

Result:
α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc E 1 μ)
⊢ ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖ =
    ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal • ‖x‖
-- Mathlib/Order/Ideal.lean
theorem top_of_top_mem (h : ⊤ ∈ I) : I = ⊤

Proof state:
case a.h
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
I : Ideal P
h : ⊤ ∈ I
x✝ : P
⊢ x✝ ∈ ↑I ↔ x✝ ∈ ↑⊤

Tactic:
exact iff_of_true (I.lower le_top h) trivial

Result:
no goals

Proof state:
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
I : Ideal P
h : ⊤ ∈ I
⊢ I = ⊤

Tactic:
ext

Result:
case a.h
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
I : Ideal P
h : ⊤ ∈ I
x✝ : P
⊢ x✝ ∈ ↑I ↔ x✝ ∈ ↑⊤
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem containsThenInsertIfNew_snd {k : α} {v : β k} :
    (m.containsThenInsertIfNew k v).2 = m.insertIfNew k v

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
v : β k
⊢ (m.containsThenInsertIfNew k v).snd = m.insertIfNew k v

Tactic:
rw [containsThenInsertIfNew_eq_insertIfNewₘ, insertIfNew_eq_insertIfNewₘ]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
theorem stepBound_pos_iff {n : ℕ} : 0 < stepBound n ↔ 0 < n :=
  mul_pos_iff_of_pos_right <| by positivity

Proof state:
n : ℕ
⊢ 0 < 4 ^ n

Tactic:
positivity

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem liftQ_mkQ (f : M →ₛₗ[τ₁₂] M₂) (h) : (p.liftQ f h).comp p.mkQ = f

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
⊢ (p.liftQ f h).comp p.mkQ = f

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
x✝ : M
⊢ ((p.liftQ f h).comp p.mkQ) x✝ = f x✝

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
x✝ : M
⊢ ((p.liftQ f h).comp p.mkQ) x✝ = f x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/SuccPred/Tree.lean
lemma RootedTree.subtrees_disjoint : t.subtrees.PairwiseDisjoint ((↑) : _ → Set t)

Proof state:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
h : t₁ ≠ t₂
⊢ ∀ ⦃a : ↑t⦄, a ∈ ↑t₁ → a ∉ ↑t₂

Tactic:
intro a ha hb

Result:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
h : t₁ ≠ t₂
a : ↑t
ha : a ∈ ↑t₁
hb : a ∈ ↑t₂
⊢ False

Proof state:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
hb : ⊥ ∈ ↑t₂
ha : t₁.root = ⊥
⊢ False

Tactic:
exact t₁.root_ne_bot_of_mem_subtrees ht₁ ha

Result:
no goals

Proof state:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
h : t₁ ≠ t₂
⊢ Function.onFun Disjoint SetLike.coe t₁ t₂

Tactic:
rw [Function.onFun_apply, Set.disjoint_left]

Result:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
h : t₁ ≠ t₂
⊢ ∀ ⦃a : ↑t⦄, a ∈ ↑t₁ → a ∉ ↑t₂

Proof state:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
h : t₁ ≠ t₂
a : ↑t
ha : a ∈ ↑t₁
hb : a ∈ ↑t₂
⊢ False

Tactic:
rw [← mem_subtrees_disjoint_iff ht₁ ht₂ a a ha hb, disjoint_self] at h

Result:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
a : ↑t
h : a = ⊥
ha : a ∈ ↑t₁
hb : a ∈ ↑t₂
⊢ False

Proof state:
t : RootedTree
⊢ t.subtrees.PairwiseDisjoint SetLike.coe

Tactic:
intro t₁ ht₁ t₂ ht₂ h

Result:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
h : t₁ ≠ t₂
⊢ Function.onFun Disjoint SetLike.coe t₁ t₂

Proof state:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
a : ↑t
h : a = ⊥
ha : a ∈ ↑t₁
hb : a ∈ ↑t₂
⊢ False

Tactic:
subst h

Result:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
ha : ⊥ ∈ ↑t₁
hb : ⊥ ∈ ↑t₂
⊢ False

Proof state:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
ha : ⊥ ∈ ↑t₁
hb : ⊥ ∈ ↑t₂
⊢ False

Tactic:
simp only [SetLike.mem_coe, SubRootedTree.bot_mem_iff] at ha

Result:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
hb : ⊥ ∈ ↑t₂
ha : t₁.root = ⊥
⊢ False
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem rightAngleRotation (z : ℂ) :
    Complex.orientation.rightAngleRotation z = I * z

Proof state:
z : ℂ
⊢ ∀ (v : ℂ), inner (Complex.orientation.rightAngleRotation z) v = inner (I * z) v

Tactic:
intro w

Result:
z w : ℂ
⊢ inner (Complex.orientation.rightAngleRotation z) w = inner (I * z) w

Proof state:
z w : ℂ
⊢ inner (Complex.orientation.rightAngleRotation z) w = inner (I * z) w

Tactic:
rw [Orientation.inner_rightAngleRotation_left]

Result:
z w : ℂ
⊢ (Complex.orientation.areaForm z) w = inner (I * z) w

Proof state:
z : ℂ
⊢ Complex.orientation.rightAngleRotation z = I * z

Tactic:
apply ext_inner_right ℝ

Result:
z : ℂ
⊢ ∀ (v : ℂ), inner (Complex.orientation.rightAngleRotation z) v = inner (I * z) v

Proof state:
z w : ℂ
⊢ (Complex.orientation.areaForm z) w = inner (I * z) w

Tactic:
simp only [Complex.areaForm, Complex.inner, mul_re, mul_im, conj_re, conj_im, map_mul, conj_I,
  neg_re, neg_im, I_re, I_im]

Result:
z w : ℂ
⊢ z.re * w.im + -z.im * w.re = (-0 * z.re - -1 * -z.im) * w.re - (-0 * -z.im + -1 * z.re) * w.im

Proof state:
z w : ℂ
⊢ z.re * w.im + -z.im * w.re = (-0 * z.re - -1 * -z.im) * w.re - (-0 * -z.im + -1 * z.re) * w.im

Tactic:
ring

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem Measurable.subtype_mk {p : β → Prop} {f : α → β} (hf : Measurable f) {h : ∀ x, p (f x)} :
    Measurable fun x => (⟨f x, h x⟩ : Subtype p) := fun t ⟨s, hs⟩ =>
  hs.2 ▸ by simp only [← preimage_comp, Function.comp_def, Subtype.coe_mk, hf hs.1]

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
p : β → Prop
f : α → β
hf : Measurable f
h : ∀ (x : α), p (f x)
t : Set (Subtype p)
x✝ : MeasurableSet t
s : Set β
hs : MeasurableSet s ∧ Subtype.val ⁻¹' s = t
⊢ MeasurableSet ((fun x => ⟨f x, ⋯⟩) ⁻¹' (Subtype.val ⁻¹' s))

Tactic:
simp only [← preimage_comp, Function.comp_def, Subtype.coe_mk, hf hs.1]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_add_of_lt {w} {x y : BitVec w} (h : x.toNat + y.toNat < 2^w) :
    (x + y).toNat = x.toNat + y.toNat

Proof state:
w : Nat
x y : BitVec w
h : x.toNat + y.toNat < 2 ^ w
⊢ (x + y).toNat = x.toNat + y.toNat

Tactic:
rw [BitVec.toNat_add, Nat.mod_eq_of_lt h]

Result:
no goals
-- Mathlib/Data/PNat/Prime.lean
theorem Coprime.gcd_mul (k : ℕ+) {m n : ℕ+} (h : m.Coprime n) :
    k.gcd (m * n) = k.gcd m * k.gcd n

Proof state:
k m n : ℕ+
h : (↑m).Coprime ↑n
⊢ k.gcd (m * n) = k.gcd m * k.gcd n

Tactic:
apply eq

Result:
case a
k m n : ℕ+
h : (↑m).Coprime ↑n
⊢ ↑(k.gcd (m * n)) = ↑(k.gcd m * k.gcd n)

Proof state:
case a
k m n : ℕ+
h : (↑m).Coprime ↑n
⊢ ↑(k.gcd (m * n)) = ↑(k.gcd m * k.gcd n)

Tactic:
simp only [gcd_coe, mul_coe]

Result:
case a
k m n : ℕ+
h : (↑m).Coprime ↑n
⊢ (↑k).gcd (↑m * ↑n) = (↑k).gcd ↑m * (↑k).gcd ↑n

Proof state:
case a
k m n : ℕ+
h : (↑m).Coprime ↑n
⊢ (↑k).gcd (↑m * ↑n) = (↑k).gcd ↑m * (↑k).gcd ↑n

Tactic:
apply Nat.Coprime.gcd_mul k h

Result:
no goals

Proof state:
k m n : ℕ+
h : m.Coprime n
⊢ k.gcd (m * n) = k.gcd m * k.gcd n

Tactic:
rw [← coprime_coe] at h

Result:
k m n : ℕ+
h : (↑m).Coprime ↑n
⊢ k.gcd (m * n) = k.gcd m * k.gcd n
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem sum_eq_iff_sum_mul_moebius_eq [Ring R] {f g : ℕ → R} :
    (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔
      ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, (μ x.fst : R) * g x.snd = f n

Proof state:
case h
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
⊢ ∀ (a : ℕ),
    a > 0 → ∑ x ∈ a.divisorsAntidiagonal, μ x.1 • g x.2 = f a ↔
      a > 0 → ∑ x ∈ a.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f a

Tactic:
refine fun a => imp_congr_right fun _ => (sum_congr rfl fun x _hx => ?_).congr_left

Result:
case h
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
a : ℕ
x✝ : a > 0
x : ℕ × ℕ
_hx : x ∈ a.divisorsAntidiagonal
⊢ μ x.1 • g x.2 = ↑(μ x.1) * g x.2

Proof state:
case h
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
a : ℕ
x✝ : a > 0
x : ℕ × ℕ
_hx : x ∈ a.divisorsAntidiagonal
⊢ μ x.1 • g x.2 = ↑(μ x.1) * g x.2

Tactic:
rw [zsmul_eq_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
⊢ (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f n

Tactic:
rw [sum_eq_iff_sum_smul_moebius_eq]

Result:
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
⊢ (∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n) ↔
    ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f n

Proof state:
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
⊢ (∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n) ↔
    ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f n

Tactic:
apply forall_congr'

Result:
case h
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
⊢ ∀ (a : ℕ),
    a > 0 → ∑ x ∈ a.divisorsAntidiagonal, μ x.1 • g x.2 = f a ↔
      a > 0 → ∑ x ∈ a.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f a
-- Mathlib/Data/Matroid/Restrict.lean
theorem restrict_eq_restrict_iff (M M' : Matroid α) (X : Set α) :
    M ↾ X = M' ↾ X ↔ ∀ I, I ⊆ X → (M.Indep I ↔ M'.Indep I)

Proof state:
case refine_2
α : Type u_1
M M' : Matroid α
X : Set α
h : ∀ I ⊆ X, M.Indep I ↔ M'.Indep I
I : Set α
hI : I ⊆ X
⊢ (M ↾ X).Indep I ↔ (M' ↾ X).Indep I

Tactic:
rw [restrict_indep_iff, and_iff_left hI, restrict_indep_iff, and_iff_left hI, h _ hI]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
M M' : Matroid α
X : Set α
h : M ↾ X = M' ↾ X
I : Set α
hIX : I ⊆ X
⊢ M.Indep I ↔ M'.Indep I

Tactic:
rw [← and_iff_left (a := (M.Indep I)) hIX, ← and_iff_left (a := (M'.Indep I)) hIX,
  ← restrict_indep_iff, h, restrict_indep_iff]

Result:
no goals

Proof state:
α : Type u_1
M M' : Matroid α
X : Set α
⊢ M ↾ X = M' ↾ X ↔ ∀ I ⊆ X, M.Indep I ↔ M'.Indep I

Tactic:
refine ⟨fun h I hIX ↦ ?_, fun h ↦ ext_indep rfl fun I (hI : I ⊆ X) ↦ ?_⟩

Result:
case refine_1
α : Type u_1
M M' : Matroid α
X : Set α
h : M ↾ X = M' ↾ X
I : Set α
hIX : I ⊆ X
⊢ M.Indep I ↔ M'.Indep I

case refine_2
α : Type u_1
M M' : Matroid α
X : Set α
h : ∀ I ⊆ X, M.Indep I ↔ M'.Indep I
I : Set α
hI : I ⊆ X
⊢ (M ↾ X).Indep I ↔ (M' ↾ X).Indep I
-- Mathlib/ModelTheory/Semantics.lean
theorem model_nonemptyTheory_iff : M ⊨ L.nonemptyTheory ↔ Nonempty M

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
⊢ M ⊨ L.nonemptyTheory ↔ Nonempty M

Tactic:
simp only [nonemptyTheory, Theory.model_iff, Set.mem_singleton_iff, forall_eq,
  Sentence.realize_cardGe, Nat.cast_one, one_le_iff_ne_zero, mk_ne_zero_iff]

Result:
no goals
-- Mathlib/Data/Rat/Floor.lean
theorem natFloor_natCast_div_natCast (n d : ℕ) : ⌊(↑n / ↑d : ℚ)⌋₊ = n / d

Proof state:
n d : ℕ
⊢ 0 ≤ ↑n / ↑d

Tactic:
positivity

Result:
no goals

Proof state:
n d : ℕ
⊢ ⌊↑n / ↑d⌋₊ = n / d

Tactic:
rw [← Int.ofNat_inj, Int.natCast_floor_eq_floor (by positivity)]

Result:
n d : ℕ
⊢ ⌊↑n / ↑d⌋ = ↑(n / d)

Proof state:
n d : ℕ
⊢ ⌊↑n / ↑d⌋ = ↑n / ↑d

Tactic:
exact floor_intCast_div_natCast n d

Result:
no goals

Proof state:
n d : ℕ
⊢ ⌊↑n / ↑d⌋ = ↑(n / d)

Tactic:
push_cast

Result:
n d : ℕ
⊢ ⌊↑n / ↑d⌋ = ↑n / ↑d
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem algEquivAevalXAddC_eq_iff {R : Type*} [CommRing R] (t t' : R) :
    algEquivAevalXAddC t = algEquivAevalXAddC t' ↔ t = t'

Proof state:
R : Type u_3
inst✝ : CommRing R
t t' : R
⊢ algEquivAevalXAddC t = algEquivAevalXAddC t' ↔ t = t'

Tactic:
simp [algEquivAevalXAddC]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
@[simp]
lemma inner_add_left {x y z : E} : ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫

Proof state:
A : Type u_1
E : Type u_2
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℂ A
inst✝⁵ : Module ℂ E
inst✝⁴ : PartialOrder A
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm A
inst✝¹ : Norm E
inst✝ : CStarModule A E
x y z : E
⊢ inner (x + y) z = inner x z + inner y z

Tactic:
rw [← star_star (r := ⟪x + y, z⟫)]

Result:
A : Type u_1
E : Type u_2
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℂ A
inst✝⁵ : Module ℂ E
inst✝⁴ : PartialOrder A
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm A
inst✝¹ : Norm E
inst✝ : CStarModule A E
x y z : E
⊢ star (star (inner (x + y) z)) = inner x z + inner y z

Proof state:
A : Type u_1
E : Type u_2
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℂ A
inst✝⁵ : Module ℂ E
inst✝⁴ : PartialOrder A
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm A
inst✝¹ : Norm E
inst✝ : CStarModule A E
x y z : E
⊢ star (star (inner (x + y) z)) = inner x z + inner y z

Tactic:
simp only [inner_add_right, star_add, star_inner]

Result:
no goals