harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem eq_zero_or_eq_zero_of_kahler_eq_zero {x y : E} (hx : o.kahler x y = 0) : x = 0 ∨ y = 0

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
⊢ x = 0 ∨ y = 0

Tactic:
rcases eq_zero_or_eq_zero_of_mul_eq_zero this with h | h

Result:
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖x‖ = 0
⊢ x = 0 ∨ y = 0

case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖y‖ = 0
⊢ x = 0 ∨ y = 0

Proof state:
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖y‖ = 0
⊢ x = 0 ∨ y = 0

Tactic:
right

Result:
case inr.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖y‖ = 0
⊢ y = 0

Proof state:
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖x‖ = 0
⊢ x = 0 ∨ y = 0

Tactic:
left

Result:
case inl.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖x‖ = 0
⊢ x = 0

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
⊢ x = 0 ∨ y = 0

Tactic:
have : ‖x‖ * ‖y‖ = 0 := by simpa [hx] using (o.norm_kahler x y).symm

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
⊢ x = 0 ∨ y = 0

Proof state:
case inl.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖x‖ = 0
⊢ x = 0

Tactic:
simpa using h

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
⊢ ‖x‖ * ‖y‖ = 0

Tactic:
simpa [hx] using (o.norm_kahler x y).symm

Result:
no goals

Proof state:
case inr.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖y‖ = 0
⊢ y = 0

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Computability/ContextFreeGrammar.lean
theorem rewrites_iff :
    r.Rewrites u v ↔ ∃ p q : List (Symbol T N),
      u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q :=
  ⟨Rewrites.exists_parts, by rintro ⟨p, q, rfl, rfl⟩; apply rewrites_of_exists_parts⟩

Proof state:
case intro.intro.intro
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
p q : List (Symbol T N)
⊢ r.Rewrites (p ++ [Symbol.nonterminal r.input] ++ q) (p ++ r.output ++ q)

Tactic:
apply rewrites_of_exists_parts

Result:
no goals

Proof state:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
⊢ (∃ p q, u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q) → r.Rewrites u v

Tactic:
rintro ⟨p, q, rfl, rfl⟩

Result:
case intro.intro.intro
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
p q : List (Symbol T N)
⊢ r.Rewrites (p ++ [Symbol.nonterminal r.input] ++ q) (p ++ r.output ++ q)
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem apply_le_nfpFamily [Small.{u} ι] [hι : Nonempty ι] (H : ∀ i, IsNormal (f i)) {a b} :
    (∀ i, f i b ≤ nfpFamily f a) ↔ b ≤ nfpFamily f a

Proof state:
case refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
hι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : b ≤ nfpFamily f a
i : ι
⊢ f i b ≤ f i (nfpFamily f a)

Tactic:
exact (H i).monotone h

Result:
no goals

Proof state:
case refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
hι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : b ≤ nfpFamily f a
i : ι
⊢ f i b ≤ nfpFamily f a

Tactic:
rw [← nfpFamily_fp (H i)]

Result:
case refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
hι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : b ≤ nfpFamily f a
i : ι
⊢ f i b ≤ f i (nfpFamily f a)

Proof state:
case refine_1
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
hι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ nfpFamily f a
⊢ b ≤ nfpFamily f a

Tactic:
obtain ⟨i⟩ := hι

Result:
case refine_1.intro
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ nfpFamily f a
i : ι
⊢ b ≤ nfpFamily f a

Proof state:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
hι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
⊢ (∀ (i : ι), f i b ≤ nfpFamily f a) ↔ b ≤ nfpFamily f a

Tactic:
refine ⟨fun h => ?_, fun h i => ?_⟩

Result:
case refine_1
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
hι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ nfpFamily f a
⊢ b ≤ nfpFamily f a

case refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
hι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : b ≤ nfpFamily f a
i : ι
⊢ f i b ≤ nfpFamily f a

Proof state:
case refine_1.intro
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ nfpFamily f a
i : ι
⊢ b ≤ nfpFamily f a

Tactic:
exact (H i).le_apply.trans (h i)

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/OfNorm.lean
theorem innerProp (r : 𝕜) : innerProp' E r

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : 𝕜
x y : E
⊢ inner_ 𝕜 (r • x) y = (starRingEnd 𝕜) r * inner_ 𝕜 x y

Tactic:
rw [← re_add_im r, add_smul, add_left, real_prop _ x, ← smul_smul, real_prop _ _ y, I_prop,
  map_add, map_mul, conj_ofReal, conj_ofReal, conj_I]

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : 𝕜
x y : E
⊢ ↑(re r) * inner_ 𝕜 x y + ↑(im r) * (-I * inner_ 𝕜 x y) = (↑(re r) + ↑(im r) * -I) * inner_ 𝕜 x y

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : 𝕜
⊢ InnerProductSpaceable.innerProp' E r

Tactic:
intro x y

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : 𝕜
x y : E
⊢ inner_ 𝕜 (r • x) y = (starRingEnd 𝕜) r * inner_ 𝕜 x y

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : 𝕜
x y : E
⊢ ↑(re r) * inner_ 𝕜 x y + ↑(im r) * (-I * inner_ 𝕜 x y) = (↑(re r) + ↑(im r) * -I) * inner_ 𝕜 x y

Tactic:
ring

Result:
no goals
-- Mathlib/Topology/Maps/Proper/Basic.lean
/-- An injective and continuous function is proper if and only if it is closed. -/
lemma isProperMap_iff_isClosedMap_of_inj (f_cont : Continuous f) (f_inj : f.Injective) :
    IsProperMap f ↔ IsClosedMap f

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : Continuous f
f_inj : Injective f
h : IsClosedMap f
⊢ Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})

Tactic:
exact ⟨f_cont, h, fun y ↦ (subsingleton_singleton.preimage f_inj).isCompact⟩

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : Continuous f
f_inj : Injective f
⊢ IsProperMap f ↔ IsClosedMap f

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

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : Continuous f
f_inj : Injective f
h : IsClosedMap f
⊢ IsProperMap f

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : Continuous f
f_inj : Injective f
h : IsClosedMap f
⊢ IsProperMap f

Tactic:
rw [isProperMap_iff_isClosedMap_and_compact_fibers]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : Continuous f
f_inj : Injective f
h : IsClosedMap f
⊢ Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma eq_one_iff_conductor_eq_one (hn : n ≠ 0) : χ = 1 ↔ conductor χ = 1

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
hn : n ≠ 0
hχ : χ.conductor = 1
⊢ χ = 1

Tactic:
obtain ⟨h', χ₀, h⟩ := factorsThrough_conductor χ

Result:
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
hn : n ≠ 0
hχ : χ.conductor = 1
h' : χ.conductor ∣ n
χ₀ : DirichletCharacter R χ.conductor
h : χ = (changeLevel h') χ₀
⊢ χ = 1

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
hn : n ≠ 0
hχ : χ.conductor = 1
h' : χ.conductor ∣ n
χ₀ : DirichletCharacter R χ.conductor
h : χ = (changeLevel h') χ₀
⊢ χ = 1

Tactic:
exact (level_one' χ₀ hχ ▸ h).trans <| changeLevel_one h'

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
hn : n ≠ 0
⊢ χ = 1 ↔ χ.conductor = 1

Tactic:
refine ⟨fun h ↦ h ▸ conductor_one hn, fun hχ ↦ ?_⟩

Result:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
hn : n ≠ 0
hχ : χ.conductor = 1
⊢ χ = 1
-- Mathlib/Probability/Distributions/Exponential.lean
/-- A negative exponential function is integrable on intervals in `R≥0` -/
lemma exp_neg_integrableOn_Ioc {b x : ℝ} (hb : 0 < b) :
    IntegrableOn (fun x ↦ rexp (-(b * x))) (Ioc 0 x)

Proof state:
b x : ℝ
hb : 0 < b
⊢ IntegrableOn (fun x => rexp (-b * x)) (Ioc 0 x) ℙ

Tactic:
exact (exp_neg_integrableOn_Ioi _ hb).mono_set Ioc_subset_Ioi_self

Result:
no goals

Proof state:
b x : ℝ
hb : 0 < b
⊢ IntegrableOn (fun x => rexp (-(b * x))) (Ioc 0 x) ℙ

Tactic:
simp only [neg_mul_eq_neg_mul]

Result:
b x : ℝ
hb : 0 < b
⊢ IntegrableOn (fun x => rexp (-b * x)) (Ioc 0 x) ℙ
-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
lemma term_sum_one (N : ℕ) : term_sum 1 N = log (N + 1) - harmonic (N + 1) + 1

Proof state:
N : ℕ
hN : ∑ n ∈ Finset.range N, term (n + 1) 1 = log (↑N + 1) - ↑(harmonic (N + 1)) + 1
⊢ 0 < N + 1

Tactic:
positivity

Result:
no goals

Proof state:
N : ℕ
⊢ term_sum 1 N = log (↑N + 1) - ↑(harmonic (N + 1)) + 1

Tactic:
induction N with
| zero =>
  simp_rw [term_sum, Finset.sum_range_zero, harmonic_succ, harmonic_zero,
    Nat.cast_zero, zero_add, Nat.cast_one, inv_one, Rat.cast_one, log_one, sub_add_cancel]
| succ N hN =>
  unfold term_sum at hN ⊢
  rw [Finset.sum_range_succ, hN, harmonic_succ (N + 1),
    term_one (by positivity : 0 < N + 1)]
  push_cast
  ring_nf

Result:
no goals

Proof state:
case succ
N : ℕ
hN : term_sum 1 N = log (↑N + 1) - ↑(harmonic (N + 1)) + 1
⊢ term_sum 1 (N + 1) = log (↑(N + 1) + 1) - ↑(harmonic (N + 1 + 1)) + 1

Tactic:
unfold term_sum at hN ⊢

Result:
case succ
N : ℕ
hN : ∑ n ∈ Finset.range N, term (n + 1) 1 = log (↑N + 1) - ↑(harmonic (N + 1)) + 1
⊢ ∑ n ∈ Finset.range (N + 1), term (n + 1) 1 = log (↑(N + 1) + 1) - ↑(harmonic (N + 1 + 1)) + 1

Proof state:
case succ
N : ℕ
hN : ∑ n ∈ Finset.range N, term (n + 1) 1 = log (↑N + 1) - ↑(harmonic (N + 1)) + 1
⊢ ∑ n ∈ Finset.range (N + 1), term (n + 1) 1 = log (↑(N + 1) + 1) - ↑(harmonic (N + 1 + 1)) + 1

Tactic:
rw [Finset.sum_range_succ, hN, harmonic_succ (N + 1),
  term_one (by positivity : 0 < N + 1)]

Result:
case succ
N : ℕ
hN : ∑ n ∈ Finset.range N, term (n + 1) 1 = log (↑N + 1) - ↑(harmonic (N + 1)) + 1
⊢ log (↑N + 1) - ↑(harmonic (N + 1)) + 1 + (log (↑(N + 1) + 1) - log ↑(N + 1) - 1 / (↑(N + 1) + 1)) =
    log (↑(N + 1) + 1) - ↑(harmonic (N + 1) + (↑(N + 1 + 1))⁻¹) + 1

Proof state:
case succ
N : ℕ
hN : ∑ n ∈ Finset.range N, term (n + 1) 1 = log (↑N + 1) - ↑(harmonic (N + 1)) + 1
⊢ log (↑N + 1) - ↑(harmonic (N + 1)) + 1 + (log (↑N + 1 + 1) - log (↑N + 1) - 1 / (↑N + 1 + 1)) =
    log (↑N + 1 + 1) - (↑(harmonic (N + 1)) + (↑N + 1 + 1)⁻¹) + 1

Tactic:
ring_nf

Result:
no goals

Proof state:
case zero

⊢ term_sum 1 0 = log (↑0 + 1) - ↑(harmonic (0 + 1)) + 1

Tactic:
simp_rw [term_sum, Finset.sum_range_zero, harmonic_succ, harmonic_zero,
  Nat.cast_zero, zero_add, Nat.cast_one, inv_one, Rat.cast_one, log_one, sub_add_cancel]

Result:
no goals

Proof state:
case succ
N : ℕ
hN : ∑ n ∈ Finset.range N, term (n + 1) 1 = log (↑N + 1) - ↑(harmonic (N + 1)) + 1
⊢ log (↑N + 1) - ↑(harmonic (N + 1)) + 1 + (log (↑(N + 1) + 1) - log ↑(N + 1) - 1 / (↑(N + 1) + 1)) =
    log (↑(N + 1) + 1) - ↑(harmonic (N + 1) + (↑(N + 1 + 1))⁻¹) + 1

Tactic:
push_cast

Result:
case succ
N : ℕ
hN : ∑ n ∈ Finset.range N, term (n + 1) 1 = log (↑N + 1) - ↑(harmonic (N + 1)) + 1
⊢ log (↑N + 1) - ↑(harmonic (N + 1)) + 1 + (log (↑N + 1 + 1) - log (↑N + 1) - 1 / (↑N + 1 + 1)) =
    log (↑N + 1 + 1) - (↑(harmonic (N + 1)) + (↑N + 1 + 1)⁻¹) + 1
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem toCNF.go_marks :
    (go aig start h state).val.cache.marks[start]'(by have := (go aig start h state).val.cache.hmarks; omega) = true :=
  (go aig start h state).property.trueAt

Proof state:
aig : AIG Nat
start : Nat
h : start < aig.decls.size
state : State aig
this : (go aig start h state).val.cache.marks.size = aig.decls.size
⊢ start < (go aig start h state).val.cache.marks.size

Tactic:
omega

Result:
no goals

Proof state:
aig : AIG Nat
start : Nat
h : start < aig.decls.size
state : State aig
⊢ start < (go aig start h state).val.cache.marks.size

Tactic:
have := (go aig start h state).val.cache.hmarks

Result:
aig : AIG Nat
start : Nat
h : start < aig.decls.size
state : State aig
this : (go aig start h state).val.cache.marks.size = aig.decls.size
⊢ start < (go aig start h state).val.cache.marks.size
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem reverse_reverse (t : RBNode α) : t.reverse.reverse = t

Proof state:
α : Type u_1
t : RBNode α
⊢ t.reverse.reverse = t

Tactic:
induction t <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem nontrivial_iff_ne_bot {N : LieSubmodule R L M} : Nontrivial N ↔ N ≠ ⊥

Proof state:
case mpr.intro
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
h : ∀ (a b : ↥N), a = b
m : M
hm : m ∈ N
⊢ m = 0

Tactic:
simpa using h ⟨m, hm⟩ ⟨_, N.zero_mem⟩

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ Nontrivial ↥N ↔ N ≠ ⊥

Tactic:
constructor <;> contrapose!

Result:
case mp
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ N = ⊥ → ¬Nontrivial ↥N

case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ ¬Nontrivial ↥N → N = ⊥

Proof state:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ ¬Nontrivial ↥N → N = ⊥

Tactic:
rw [not_nontrivial_iff_subsingleton, LieSubmodule.eq_bot_iff]

Result:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ Subsingleton ↥N → ∀ m ∈ N, m = 0

Proof state:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ Subsingleton ↥N → ∀ m ∈ N, m = 0

Tactic:
rintro ⟨h⟩ m hm

Result:
case mpr.intro
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
h : ∀ (a b : ↥N), a = b
m : M
hm : m ∈ N
⊢ m = 0

Proof state:
case mp.mk.intro.mk.intro.mk
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m₁ : M
h₁ : m₁ ∈ ⊥
m₂ : M
h₂ : m₂ ∈ ⊥
h₁₂ : ⟨m₁, h₁⟩ ≠ ⟨m₂, h₂⟩
⊢ False

Tactic:
simp [(LieSubmodule.mem_bot _).mp h₁, (LieSubmodule.mem_bot _).mp h₂] at h₁₂

Result:
no goals

Proof state:
case mp
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ N = ⊥ → ¬Nontrivial ↥N

Tactic:
rintro rfl
  ⟨⟨m₁, h₁ : m₁ ∈ (⊥ : LieSubmodule R L M)⟩, ⟨m₂, h₂ : m₂ ∈ (⊥ : LieSubmodule R L M)⟩, h₁₂⟩

Result:
case mp.mk.intro.mk.intro.mk
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m₁ : M
h₁ : m₁ ∈ ⊥
m₂ : M
h₂ : m₂ ∈ ⊥
h₁₂ : ⟨m₁, h₁⟩ ≠ ⟨m₂, h₂⟩
⊢ False
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem add_zero' (x : LocalizedModule S M) : x + 0 = x :=
  induction_on
    (fun m s => by
      rw [← zero_mk s, mk_add_mk, smul_zero, add_zero, mk_eq]
      exact ⟨1, by rw [one_smul, mul_smul, one_smul]⟩)
    x

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : LocalizedModule S M
m : M
s : ↥S
⊢ ∃ u, u • s • s • m = u • (s * s) • m

Tactic:
exact ⟨1, by rw [one_smul, mul_smul, one_smul]⟩

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : LocalizedModule S M
m : M
s : ↥S
⊢ 1 • s • s • m = 1 • (s * s) • m

Tactic:
rw [one_smul, mul_smul, one_smul]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : LocalizedModule S M
m : M
s : ↥S
⊢ mk m s + 0 = mk m s

Tactic:
rw [← zero_mk s, mk_add_mk, smul_zero, add_zero, mk_eq]

Result:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : LocalizedModule S M
m : M
s : ↥S
⊢ ∃ u, u • s • s • m = u • (s * s) • m
-- Mathlib/Data/ZMod/Basic.lean
theorem val_lt {n : ℕ} [NeZero n] (a : ZMod n) : a.val < n

Proof state:
case zero
inst✝ : NeZero 0
a : ZMod 0
⊢ a.val < 0

Tactic:
cases NeZero.ne 0 rfl

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ a.val < n

Tactic:
cases n

Result:
case zero
inst✝ : NeZero 0
a : ZMod 0
⊢ a.val < 0

case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a : ZMod (n✝ + 1)
⊢ a.val < n✝ + 1

Proof state:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a : ZMod (n✝ + 1)
⊢ a.val < n✝ + 1

Tactic:
exact Fin.is_lt a

Result:
no goals
-- Mathlib/GroupTheory/FiniteAbelian/Duality.lean
theorem exists_apply_ne_one_of_hasEnoughRootsOfUnity {a : G} (ha : a ≠ 1) :
    ∃ φ : G →* Mˣ, φ a ≠ 1

Proof state:
G : Type u_1
M : Type u_2
inst✝³ : CommGroup G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
a✝ : G
ha : a✝ ≠ 1
n : ℕ
hn : n ∣ Monoid.exponent G
a : ZMod n
ha₀ : a ≠ 0
this : NeZero n
⊢ ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1

Tactic:
have := HasEnoughRootsOfUnity.of_dvd M hn

Result:
G : Type u_1
M : Type u_2
inst✝³ : CommGroup G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
a✝ : G
ha : a✝ ≠ 1
n : ℕ
hn : n ∣ Monoid.exponent G
a : ZMod n
ha₀ : a ≠ 0
this✝ : NeZero n
this : HasEnoughRootsOfUnity M n
⊢ ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1

Proof state:
G : Type u_1
M : Type u_2
inst✝³ : CommGroup G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
a✝ : G
ha : a✝ ≠ 1
n : ℕ
hn : n ∣ Monoid.exponent G
a : ZMod n
ha₀ : a ≠ 0
⊢ ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1

Tactic:
have : NeZero n := ⟨fun H ↦ NeZero.ne _ <| Nat.eq_zero_of_zero_dvd (H ▸ hn)⟩

Result:
G : Type u_1
M : Type u_2
inst✝³ : CommGroup G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
a✝ : G
ha : a✝ ≠ 1
n : ℕ
hn : n ∣ Monoid.exponent G
a : ZMod n
ha₀ : a ≠ 0
this : NeZero n
⊢ ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1

Proof state:
G : Type u_1
M : Type u_2
inst✝³ : CommGroup G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
a✝ : G
ha : a✝ ≠ 1
n : ℕ
hn : n ∣ Monoid.exponent G
a : ZMod n
ha₀ : a ≠ 0
this✝ : NeZero n
this : HasEnoughRootsOfUnity M n
⊢ ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1

Tactic:
exact ZMod.exists_monoidHom_apply_ne_one (HasEnoughRootsOfUnity.exists_primitiveRoot M n) ha₀

Result:
no goals

Proof state:
G : Type u_1
M : Type u_2
inst✝³ : CommGroup G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
a : G
ha : a ≠ 1
⊢ ∃ φ, φ a ≠ 1

Tactic:
refine exists_apply_ne_one_aux G Mˣ (fun n hn a ha₀ ↦ ?_) ha

Result:
G : Type u_1
M : Type u_2
inst✝³ : CommGroup G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
a✝ : G
ha : a✝ ≠ 1
n : ℕ
hn : n ∣ Monoid.exponent G
a : ZMod n
ha₀ : a ≠ 0
⊢ ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem or_and_distrib_left (x y z : Nat) : x ||| (y &&& z) = (x ||| y) &&& (x ||| z)

Proof state:
x y z : Nat
⊢ x ||| y &&& z = (x ||| y) &&& (x ||| z)

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
x y z : Nat
⊢ ∀ (i : Nat), (x ||| y &&& z).testBit i = ((x ||| y) &&& (x ||| z)).testBit i

Proof state:
case pred
x y z : Nat
⊢ ∀ (i : Nat), (x ||| y &&& z).testBit i = ((x ||| y) &&& (x ||| z)).testBit i

Tactic:
simp [Bool.or_and_distrib_left]

Result:
no goals