harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Fintype/BigOperators.lean
theorem prod_bool [CommMonoid α] (f : Bool → α) : ∏ b, f b = f true * f false

Proof state:
α : Type u_1
inst✝ : CommMonoid α
f : Bool → α
⊢ ∏ b : Bool, f b = f true * f false

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
/-- Let `p` and `q` be two seminorms on a vector space over a `NontriviallyNormedField`.
If we have `q x ≤ C * p x` on some shell of the form `{x | ε/‖c‖ ≤ p x < ε}` (where `ε > 0`
and `‖c‖ > 1`), then we also have `q x ≤ C * p x` for all `x` such that `p x ≠ 0`. -/
lemma bound_of_shell
    (p q : Seminorm 𝕜 E) {ε C : ℝ} (ε_pos : 0 < ε) {c : 𝕜} (hc : 1 < ‖c‖)
    (hf : ∀ x, ε / ‖c‖ ≤ p x → p x < ε → q x ≤ C * p x) {x : E} (hx : p x ≠ 0) :
    q x ≤ C * p x

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ p x → p x < ε → q x ≤ C * p x
x : E
hx : p x ≠ 0
⊢ q x ≤ C * p x

Tactic:
rcases p.rescale_to_shell hc ε_pos hx with ⟨δ, hδ, δxle, leδx, -⟩

Result:
case intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ p x → p x < ε → q x ≤ C * p x
x : E
hx : p x ≠ 0
δ : 𝕜
hδ : δ ≠ 0
δxle : p (δ • x) < ε
leδx : ε / ‖c‖ ≤ p (δ • x)
⊢ q x ≤ C * p x

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ p x → p x < ε → q x ≤ C * p x
x : E
hx : p x ≠ 0
δ : 𝕜
hδ : δ ≠ 0
δxle : p (δ • x) < ε
leδx : ε / ‖c‖ ≤ p (δ • x)
⊢ q x ≤ C * p x

Tactic:
simpa only [map_smul_eq_mul, mul_left_comm C, mul_le_mul_left (norm_pos_iff.2 hδ)]
  using hf (δ • x) leδx δxle

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_intCast {n : ℕ} (a : ℤ) [NeZero n] : ↑(a : ZMod n).val = a % n

Proof state:
n : ℕ
a : ℤ
inst✝ : NeZero n
⊢ ↑(↑a).val = a % ↑n

Tactic:
have hle : (0 : ℤ) ≤ ↑(a : ZMod n).val := Int.natCast_nonneg _

Result:
n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(↑a).val
⊢ ↑(↑a).val = a % ↑n

Proof state:
n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(↑a).val
hlt : ↑(↑a).val < ↑n
⊢ ↑(↑a).val % ↑n = a % ↑n

Tactic:
rw [← ZMod.intCast_eq_intCast_iff', Int.cast_natCast, ZMod.natCast_val, ZMod.cast_id]

Result:
no goals

Proof state:
n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(↑a).val
hlt : ↑(↑a).val < ↑n
⊢ ↑(↑a).val = a % ↑n

Tactic:
refine (Int.emod_eq_of_lt hle hlt).symm.trans ?_

Result:
n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(↑a).val
hlt : ↑(↑a).val < ↑n
⊢ ↑(↑a).val % ↑n = a % ↑n

Proof state:
n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(↑a).val
⊢ ↑(↑a).val = a % ↑n

Tactic:
have hlt : ↑(a : ZMod n).val < (n : ℤ) := Int.ofNat_lt.mpr (ZMod.val_lt a)

Result:
n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(↑a).val
hlt : ↑(↑a).val < ↑n
⊢ ↑(↑a).val = a % ↑n
-- Mathlib/GroupTheory/Sylow.lean
theorem card_sylow_modEq_one [Fact p.Prime] [Finite (Sylow p G)] :
    Nat.card (Sylow p G) ≡ 1 [MOD p]

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this✝ : fixedPoints (↥↑P) (Sylow p G) = {P}
this : Nat.card ↑(fixedPoints (↥↑P) (Sylow p G)) = 1
⊢ Nat.card ↑(fixedPoints (↥↑P) (Sylow p G)) ≡ 1 [MOD p]

Tactic:
rw [this]

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this : fixedPoints (↥↑P) (Sylow p G) = {P}
⊢ Nat.card ↑(fixedPoints (↥↑P) (Sylow p G)) = 1

Tactic:
simp [this]

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this : fixedPoints (↥↑P) (Sylow p G) = {P}
⊢ Nat.card (Sylow p G) ≡ 1 [MOD p]

Tactic:
have : Nat.card (fixedPoints P.1 (Sylow p G)) = 1 := by simp [this]

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this✝ : fixedPoints (↥↑P) (Sylow p G) = {P}
this : Nat.card ↑(fixedPoints (↥↑P) (Sylow p G)) = 1
⊢ Nat.card (Sylow p G) ≡ 1 [MOD p]

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
⊢ Nat.card (Sylow p G) ≡ 1 [MOD p]

Tactic:
have : fixedPoints P.1 (Sylow p G) = {P} :=
  Set.ext fun Q : Sylow p G =>
    calc
      Q ∈ fixedPoints P (Sylow p G) ↔ P.1 ≤ Q := P.2.sylow_mem_fixedPoints_iff
      _ ↔ Q.1 = P.1 := ⟨P.3 Q.2, ge_of_eq⟩
      _ ↔ Q ∈ {P} := Sylow.ext_iff.symm.trans Set.mem_singleton_iff.symm

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this : fixedPoints (↥↑P) (Sylow p G) = {P}
⊢ Nat.card (Sylow p G) ≡ 1 [MOD p]

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this✝ : fixedPoints (↥↑P) (Sylow p G) = {P}
this : Nat.card ↑(fixedPoints (↥↑P) (Sylow p G)) = 1
⊢ Nat.card (Sylow p G) ≡ 1 [MOD p]

Tactic:
exact (P.2.card_modEq_card_fixedPoints (Sylow p G)).trans (by rw [this])

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
⊢ Nat.card (Sylow p G) ≡ 1 [MOD p]

Tactic:
refine Sylow.nonempty.elim fun P : Sylow p G => ?_

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
⊢ Nat.card (Sylow p G) ≡ 1 [MOD p]
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem IsCyclic.exponent_eq_card [Group α] [IsCyclic α] :
    exponent α = Nat.card α

Proof state:
case intro
α : Type u_1
inst✝¹ : Group α
inst✝ : IsCyclic α
g : α
hg : orderOf g = Nat.card α
⊢ exponent α = Nat.card α

Tactic:
apply Nat.dvd_antisymm Group.exponent_dvd_nat_card

Result:
case intro
α : Type u_1
inst✝¹ : Group α
inst✝ : IsCyclic α
g : α
hg : orderOf g = Nat.card α
⊢ Nat.card α ∣ exponent α

Proof state:
case intro
α : Type u_1
inst✝¹ : Group α
inst✝ : IsCyclic α
g : α
hg : orderOf g = Nat.card α
⊢ Nat.card α ∣ exponent α

Tactic:
rw [← hg]

Result:
case intro
α : Type u_1
inst✝¹ : Group α
inst✝ : IsCyclic α
g : α
hg : orderOf g = Nat.card α
⊢ orderOf g ∣ exponent α

Proof state:
α : Type u_1
inst✝¹ : Group α
inst✝ : IsCyclic α
⊢ exponent α = Nat.card α

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := α)

Result:
case intro
α : Type u_1
inst✝¹ : Group α
inst✝ : IsCyclic α
g : α
hg : orderOf g = Nat.card α
⊢ exponent α = Nat.card α

Proof state:
case intro
α : Type u_1
inst✝¹ : Group α
inst✝ : IsCyclic α
g : α
hg : orderOf g = Nat.card α
⊢ orderOf g ∣ exponent α

Tactic:
exact order_dvd_exponent _

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma IsBase.exchange_base_of_not_mem_closure (hB : M.IsBase B) (he : e ∈ B)
    (hf : f ∉ M.closure (B \ {e})) (hfE : f ∈ M.E

Proof state:
case inl
α : Type u_2
M : Matroid α
f : α
B : Set α
hB : M.IsBase B
hfE : autoParam (f ∈ M.E) _auto✝
he : f ∈ B
hf : f ∉ M.closure (B \ {f})
⊢ M.IsBase (insert f (B \ {f}))

Tactic:
simpa [he]

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : autoParam (f ∈ M.E) _auto✝
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
obtain rfl | hne := eq_or_ne f e

Result:
case inl
α : Type u_2
M : Matroid α
f : α
B : Set α
hB : M.IsBase B
hfE : autoParam (f ∈ M.E) _auto✝
he : f ∈ B
hf : f ∉ M.closure (B \ {f})
⊢ M.IsBase (insert f (B \ {f}))

case inr
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : autoParam (f ∈ M.E) _auto✝
hne : f ≠ e
⊢ M.IsBase (insert f (B \ {e}))

Proof state:
case inr
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : autoParam (f ∈ M.E) _auto✝
hne : f ≠ e
hi : M.Indep (insert f (B \ {e}))
hfB : f ∉ B
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
exact hB.exchange_isBase_of_indep hfB hi

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : autoParam (f ∈ M.E) _auto✝
hne : f ≠ e
⊢ M.Indep (insert f (B \ {e})) ∧ f ∉ B

Tactic:
simpa [(hB.indep.diff _).not_mem_closure_iff, hne] using hf

Result:
no goals

Proof state:
case inr
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : autoParam (f ∈ M.E) _auto✝
hne : f ≠ e
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
have ⟨hi, hfB⟩ : M.Indep (insert f (B \ {e})) ∧ f ∉ B := by
  simpa [(hB.indep.diff _).not_mem_closure_iff, hne] using hf

Result:
case inr
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : autoParam (f ∈ M.E) _auto✝
hne : f ≠ e
hi : M.Indep (insert f (B \ {e}))
hfB : f ∉ B
⊢ M.IsBase (insert f (B \ {e}))
-- Mathlib/AlgebraicGeometry/ValuativeCriterion.lean
@[stacks 01KE]
protected lemma eq :
    ValuativeCriterion.Existence = (topologically @SpecializingMap).universally

Proof state:
case h.mp.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
a✝ : Existence f✝
⊢ ?h.mp.a ≤ topologically @SpecializingMap

Tactic:
apply specializingMap

Result:
no goals

Proof state:
case h.mp.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
a✝ : Existence f✝
⊢ Existence.universally f✝

Tactic:
rwa [MorphismProperty.IsStableUnderBaseChange.universally_eq]

Result:
no goals

Proof state:
case h
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ Existence f✝ ↔ (topologically @SpecializingMap).universally f✝

Tactic:
constructor

Result:
case h.mp
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ Existence f✝ → (topologically @SpecializingMap).universally f✝

case h.mpr
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ (topologically @SpecializingMap).universally f✝ → Existence f✝

Proof state:
case h.mp
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
a✝ : Existence f✝
⊢ (topologically @SpecializingMap).universally f✝

Tactic:
apply MorphismProperty.universally_mono

Result:
case h.mp.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
a✝ : Existence f✝
⊢ ?h.mp.a ≤ topologically @SpecializingMap

case h.mp.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
a✝ : Existence f✝
⊢ MorphismProperty.universally ?h.mp.a f✝

case h.mp.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
a✝ : Existence f✝
⊢ MorphismProperty Scheme

Proof state:
⊢ Existence = (topologically @SpecializingMap).universally

Tactic:
ext

Result:
case h
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ Existence f✝ ↔ (topologically @SpecializingMap).universally f✝

Proof state:
case h.mp
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ Existence f✝ → (topologically @SpecializingMap).universally f✝

Tactic:
intro _

Result:
case h.mp
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
a✝ : Existence f✝
⊢ (topologically @SpecializingMap).universally f✝

Proof state:
case h.mpr
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ (topologically @SpecializingMap).universally f✝ → Existence f✝

Tactic:
apply of_specializingMap

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem sin_eq_zero_iff {θ : ℂ} : sin θ = 0 ↔ ∃ k : ℤ, θ = k * π

Proof state:
case h
k : ℤ
⊢ ↑k * ↑π - ↑π / 2 = (2 * ↑(k - 1) + 1) * ↑π / 2

Tactic:
field_simp

Result:
case h
k : ℤ
⊢ ↑k * ↑π * 2 - ↑π = (2 * (↑k - 1) + 1) * ↑π

Proof state:
case h
k : ℤ
⊢ ↑k * ↑π * 2 - ↑π = (2 * (↑k - 1) + 1) * ↑π

Tactic:
ring

Result:
no goals

Proof state:
θ : ℂ
⊢ (∃ k, θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2) ↔ ∃ k, θ = ↑k * ↑π

Tactic:
constructor

Result:
case mp
θ : ℂ
⊢ (∃ k, θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2) → ∃ k, θ = ↑k * ↑π

case mpr
θ : ℂ
⊢ (∃ k, θ = ↑k * ↑π) → ∃ k, θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2

Proof state:
case mp.intro
θ : ℂ
k : ℤ
hk : θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2
⊢ ∃ k, θ = ↑k * ↑π

Tactic:
use k + 1

Result:
case h
θ : ℂ
k : ℤ
hk : θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2
⊢ θ = ↑(k + 1) * ↑π

Proof state:
case mpr.intro
k : ℤ
⊢ ∃ k_1, ↑k * ↑π - ↑π / 2 = (2 * ↑k_1 + 1) * ↑π / 2

Tactic:
use k - 1

Result:
case h
k : ℤ
⊢ ↑k * ↑π - ↑π / 2 = (2 * ↑(k - 1) + 1) * ↑π / 2

Proof state:
case mpr
θ : ℂ
⊢ (∃ k, θ = ↑k * ↑π) → ∃ k, θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2

Tactic:
rintro ⟨k, rfl⟩

Result:
case mpr.intro
k : ℤ
⊢ ∃ k_1, ↑k * ↑π - ↑π / 2 = (2 * ↑k_1 + 1) * ↑π / 2

Proof state:
case h
θ : ℂ
k : ℤ
hk : θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2
⊢ (2 * ↑k + 1) * ↑π + ↑π = (↑k + 1) * ↑π * 2

Tactic:
ring

Result:
no goals

Proof state:
case mp
θ : ℂ
⊢ (∃ k, θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2) → ∃ k, θ = ↑k * ↑π

Tactic:
rintro ⟨k, hk⟩

Result:
case mp.intro
θ : ℂ
k : ℤ
hk : θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2
⊢ ∃ k, θ = ↑k * ↑π

Proof state:
case h
θ : ℂ
k : ℤ
hk : θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2
⊢ θ = ↑(k + 1) * ↑π

Tactic:
field_simp [eq_add_of_sub_eq hk]

Result:
case h
θ : ℂ
k : ℤ
hk : θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2
⊢ (2 * ↑k + 1) * ↑π + ↑π = (↑k + 1) * ↑π * 2

Proof state:
θ : ℂ
⊢ sin θ = 0 ↔ ∃ k, θ = ↑k * ↑π

Tactic:
rw [← Complex.cos_sub_pi_div_two, cos_eq_zero_iff]

Result:
θ : ℂ
⊢ (∃ k, θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2) ↔ ∃ k, θ = ↑k * ↑π
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem map_zipWithAll {δ : Type _} (f : α → β) (g : Option γ → Option δ → α) (l : List γ) (l' : List δ) :
    map f (zipWithAll g l l') = zipWithAll (fun x y => f (g x y)) l l'

Proof state:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : Option γ → Option δ → α
l' : List δ
⊢ map f (zipWithAll g [] l') = zipWithAll (fun x y => f (g x y)) [] l'

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : Option γ → Option δ → α
hd : γ
tl : List γ
hl : ∀ (l' : List δ), map f (zipWithAll g tl l') = zipWithAll (fun x y => f (g x y)) tl l'
l' : List δ
⊢ map f (zipWithAll g (hd :: tl) l') = zipWithAll (fun x y => f (g x y)) (hd :: tl) l'

Tactic:
cases l' <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : Option γ → Option δ → α
l : List γ
l' : List δ
⊢ map f (zipWithAll g l l') = zipWithAll (fun x y => f (g x y)) l l'

Tactic:
induction l generalizing l' with
| nil => simp
| cons hd tl hl =>
  cases l' <;> simp_all

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
@[to_additive (attr := simp) existing zmod_val_inv_nsmul_nsmul]
lemma pow_pow_zmod_val_inv (hn : (Nat.card α).Coprime n) (a : α) :
    (a ^ n) ^ (n⁻¹ : ZMod (Nat.card α)).val = a

Proof state:
α : Type u_1
inst✝ : Group α
n : ℕ
hn : (Nat.card α).Coprime n
a : α
⊢ (a ^ n) ^ (↑n)⁻¹.val = a

Tactic:
rw [pow_right_comm, pow_zmod_val_inv_pow hn]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem node3L_size {l x m y r} : size (@node3L α l x m y r) = size l + size m + size r + 2

Proof state:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (((match l with
            | nil => 0
            | node sz l x r => sz) +
            match m with
            | nil => 0
            | node sz l x r => sz) +
          1 +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      1 =
    (((match l with
          | nil => 0
          | node sz l x r => sz) +
          match m with
          | nil => 0
          | node sz l x r => sz) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      2

Tactic:
rw [add_right_comm _ 1]

Result:
no goals

Proof state:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node3L x m y r).size = l.size + m.size + r.size + 2

Tactic:
dsimp [node3L, node', size]

Result:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (((match l with
            | nil => 0
            | node sz l x r => sz) +
            match m with
            | nil => 0
            | node sz l x r => sz) +
          1 +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      1 =
    (((match l with
          | nil => 0
          | node sz l x r => sz) +
          match m with
          | nil => 0
          | node sz l x r => sz) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      2
-- Mathlib/RingTheory/Ideal/Basic.lean
theorem isField_iff_isSimpleOrder_ideal : IsField R ↔ IsSimpleOrder (Ideal R)

Proof state:
case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (∀ (I : Ideal R), ⊥ < I → ¬I < ⊤) ↔ IsSimpleOrder (Ideal R)

Tactic:
simp_rw [lt_top_iff_ne_top, bot_lt_iff_ne_bot, ← or_iff_not_imp_left, not_ne_iff]

Result:
case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (∀ (I : Ideal R), I = ⊥ ∨ I = ⊤) ↔ IsSimpleOrder (Ideal R)

Proof state:
R : Type u_5
inst✝ : CommSemiring R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)

Tactic:
cases subsingleton_or_nontrivial R

Result:
case inl
R : Type u_5
inst✝ : CommSemiring R
h✝ : Subsingleton R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)

case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)

Proof state:
case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (∀ (I : Ideal R), I = ⊥ ∨ I = ⊤) ↔ IsSimpleOrder (Ideal R)

Tactic:
exact ⟨fun h => ⟨h⟩, fun h => h.2⟩

Result:
no goals

Proof state:
case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (¬∃ I, ⊥ < I ∧ I < ⊤) ↔ ¬¬IsSimpleOrder (Ideal R)

Tactic:
push_neg

Result:
case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (∀ (I : Ideal R), ⊥ < I → ¬I < ⊤) ↔ IsSimpleOrder (Ideal R)

Proof state:
case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)

Tactic:
rw [← not_iff_not, Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top, ← not_iff_not]

Result:
case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (¬∃ I, ⊥ < I ∧ I < ⊤) ↔ ¬¬IsSimpleOrder (Ideal R)

Proof state:
case inl
R : Type u_5
inst✝ : CommSemiring R
h✝ : Subsingleton R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)

Tactic:
exact
  ⟨fun h => (not_isField_of_subsingleton _ h).elim, fun h =>
    (false_of_nontrivial_of_subsingleton <| Ideal R).elim⟩

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
lemma mul_le_of_forall_lt {a b c : ℝ≥0∞} (h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c) : a * b ≤ c

Proof state:
case intro.intro.intro.intro
a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
d : ℝ≥0∞
hd✝¹ : d < a * b
a' : ℝ≥0∞
ha' : a' < a
hd✝ : d < a' * b
b' : ℝ≥0∞
hb' : b' < b
hd : d < a' * b'
⊢ d ≤ c

Tactic:
exact le_trans hd.le <| h _ ha' _ hb'

Result:
no goals

Proof state:
case intro.intro
a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
d : ℝ≥0∞
hd✝ : d < a * b
a' : ℝ≥0∞
ha' : a' < a
hd : d < a' * b
⊢ d ≤ c

Tactic:
obtain ⟨b', hb', hd⟩ := exists_lt_mul_right hd

Result:
case intro.intro.intro.intro
a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
d : ℝ≥0∞
hd✝¹ : d < a * b
a' : ℝ≥0∞
ha' : a' < a
hd✝ : d < a' * b
b' : ℝ≥0∞
hb' : b' < b
hd : d < a' * b'
⊢ d ≤ c

Proof state:
a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
⊢ a * b ≤ c

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_

Result:
a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
d : ℝ≥0∞
hd : d < a * b
⊢ d ≤ c

Proof state:
a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
d : ℝ≥0∞
hd : d < a * b
⊢ d ≤ c

Tactic:
obtain ⟨a', ha', hd⟩ := exists_lt_mul_left hd

Result:
case intro.intro
a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
d : ℝ≥0∞
hd✝ : d < a * b
a' : ℝ≥0∞
ha' : a' < a
hd : d < a' * b
⊢ d ≤ c
-- Mathlib/Algebra/GroupWithZero/Indicator.lean
lemma support_mul_subset_right (f g : ι → M₀) : support (fun x ↦ f x * g x) ⊆ support g :=
  fun x hfg hg => hfg <| by simp only [hg, mul_zero]

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
f g : ι → M₀
x : ι
hfg : x ∈ support fun x => f x * g x
hg : g x = 0
⊢ (fun x => f x * g x) x = 0

Tactic:
simp only [hg, mul_zero]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem mem_iInf {ι : Sort*} {S : ι → Subgroup G} {x : G} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i

Proof state:
G : Type u_1
inst✝ : Group G
ι : Sort u_2
S : ι → Subgroup G
x : G
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem lex_eq_decide_lex [DecidableEq α] (lt : α → α → Bool) :
    lex l₁ l₂ lt = decide (Lex (fun x y => lt x y) l₁ l₂)

Proof state:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
lt : α → α → Bool
a : α
l₁ : List α
ih : ∀ {l₂ : List α}, l₁.lex l₂ lt = decide (Lex (fun x y => lt x y = true) l₁ l₂)
⊢ (a :: l₁).lex [] lt = decide (Lex (fun x y => lt x y = true) (a :: l₁) [])

Tactic:
simp [lex]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
lt : α → α → Bool
l₂ : List α
⊢ [].lex l₂ lt = decide (Lex (fun x y => lt x y = true) [] l₂)

Tactic:
cases l₂ with
| nil => simp [lex]
| cons b bs => simp [lex]

Result:
no goals

Proof state:
case nil.cons
α : Type u_1
inst✝ : DecidableEq α
lt : α → α → Bool
b : α
bs : List α
⊢ [].lex (b :: bs) lt = decide (Lex (fun x y => lt x y = true) [] (b :: bs))

Tactic:
simp [lex]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
lt : α → α → Bool
a : α
l₁ : List α
ih : ∀ {l₂ : List α}, l₁.lex l₂ lt = decide (Lex (fun x y => lt x y = true) l₁ l₂)
l₂ : List α
⊢ (a :: l₁).lex l₂ lt = decide (Lex (fun x y => lt x y = true) (a :: l₁) l₂)

Tactic:
cases l₂ with
| nil => simp [lex]
| cons b bs =>
  simp [lex, ih, cons_lex_cons_iff, Bool.beq_eq_decide_eq]

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
lt : α → α → Bool
a : α
l₁ : List α
ih : ∀ {l₂ : List α}, l₁.lex l₂ lt = decide (Lex (fun x y => lt x y = true) l₁ l₂)
b : α
bs : List α
⊢ (a :: l₁).lex (b :: bs) lt = decide (Lex (fun x y => lt x y = true) (a :: l₁) (b :: bs))

Tactic:
simp [lex, ih, cons_lex_cons_iff, Bool.beq_eq_decide_eq]

Result:
no goals

Proof state:
case nil.nil
α : Type u_1
inst✝ : DecidableEq α
lt : α → α → Bool
⊢ [].lex [] lt = decide (Lex (fun x y => lt x y = true) [] [])

Tactic:
simp [lex]

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
lt : α → α → Bool
⊢ l₁.lex l₂ lt = decide (Lex (fun x y => lt x y = true) l₁ l₂)

Tactic:
induction l₁ generalizing l₂ with
| nil =>
  cases l₂ with
  | nil => simp [lex]
  | cons b bs => simp [lex]
| cons a l₁ ih =>
  cases l₂ with
  | nil => simp [lex]
  | cons b bs =>
    simp [lex, ih, cons_lex_cons_iff, Bool.beq_eq_decide_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
@[simp]
lemma zeroEquiv_ιMulti (f : Fin 0 → M) :
    zeroEquiv R M (ιMulti _ _ f) = 1

Proof state:
R : Type u
inst✝² : CommRing R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : Fin 0 → M
⊢ (zeroEquiv R M) ((ιMulti R 0) f) = 1

Tactic:
simp [zeroEquiv]

Result:
no goals
-- Mathlib/Topology/Filter.lean
theorem nhds_iInf (f : ι → Filter α) : 𝓝 (⨅ i, f i) = ⨅ i, 𝓝 (f i)

Proof state:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ (⨅ i, f i).lift' (Iic ∘ 𝓟) = ⨅ i, (f i).lift' (Iic ∘ 𝓟)

Tactic:
apply lift'_iInf_of_map_univ <;> simp

Result:
no goals

Proof state:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ 𝓝 (⨅ i, f i) = ⨅ i, 𝓝 (f i)

Tactic:
simp only [nhds_eq]

Result:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ (⨅ i, f i).lift' (Iic ∘ 𝓟) = ⨅ i, (f i).lift' (Iic ∘ 𝓟)
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem Bornology.IsBounded.inv : IsBounded s → IsBounded s⁻¹

Proof state:
E : Type u_1
inst✝ : SeminormedGroup E
s : Set E
⊢ (∃ C, ∀ ⦃x : E⦄, x ∈ s → ‖x‖ ≤ C) → ∃ C, ∀ ⦃x : E⦄, x ∈ s → ‖x‖ ≤ C

Tactic:
exact id

Result:
no goals

Proof state:
E : Type u_1
inst✝ : SeminormedGroup E
s : Set E
⊢ IsBounded s → IsBounded s⁻¹

Tactic:
simp_rw [isBounded_iff_forall_norm_le', ← image_inv_eq_inv, forall_mem_image, norm_inv']

Result:
E : Type u_1
inst✝ : SeminormedGroup E
s : Set E
⊢ (∃ C, ∀ ⦃x : E⦄, x ∈ s → ‖x‖ ≤ C) → ∃ C, ∀ ⦃x : E⦄, x ∈ s → ‖x‖ ≤ C