harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Factorization/Root.lean
/-- Galois connection between `a ↦ a ^ n : ℕ → ℕ` and `floorRoot n : ℕ → ℕ` where `ℕ` is ordered
by divisibility. -/
lemma pow_dvd_iff_dvd_floorRoot : a ^ n ∣ b ↔ a ∣ floorRoot n b

Proof state:
case inr.inr.inr
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
rw [← factorization_le_iff_dvd (pow_ne_zero _ ha) hb,
  ← factorization_le_iff_dvd ha (floorRoot_ne_zero.2 ⟨hn, hb⟩), factorization_pow,
  factorization_floorRoot, le_floorDiv_iff_smul_le (β := ℕ →₀ ℕ) (pos_iff_ne_zero.2 hn)]

Result:
no goals

Proof state:
case inr.inr
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
obtain rfl | ha := eq_or_ne a 0

Result:
case inr.inr.inl
b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
⊢ 0 ^ n ∣ b ↔ 0 ∣ n.floorRoot b

case inr.inr.inr
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Proof state:
case inr.inl
a n : ℕ
hn : n ≠ 0
⊢ a ^ n ∣ 0 ↔ a ∣ n.floorRoot 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
a b n : ℕ
hn : n ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
obtain rfl | hb := eq_or_ne b 0

Result:
case inr.inl
a n : ℕ
hn : n ≠ 0
⊢ a ^ n ∣ 0 ↔ a ∣ n.floorRoot 0

case inr.inr
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Proof state:
a b n : ℕ
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
obtain rfl | hn := eq_or_ne n 0

Result:
case inl
a b : ℕ
⊢ a ^ 0 ∣ b ↔ a ∣ floorRoot 0 b

case inr
a b n : ℕ
hn : n ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Proof state:
case inr.inr.inl
b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
⊢ 0 ^ n ∣ b ↔ 0 ∣ n.floorRoot b

Tactic:
simp [hn]

Result:
no goals

Proof state:
case inl
a b : ℕ
⊢ a ^ 0 ∣ b ↔ a ∣ floorRoot 0 b

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
    a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
⊢ a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m

Tactic:
simp [mem_iff_contains, contains_erase h]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem mul_neg_of_pos_of_neg [PosMulStrictMono α] (ha : 0 < a) (hb : b < 0) : a * b < 0

Proof state:
α : Type u_3
a b : α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
ha : 0 < a
hb : b < 0
⊢ a * b < 0

Tactic:
simpa only [mul_zero] using mul_lt_mul_of_pos_left hb ha

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Discriminant/Defs.lean
theorem numberField_discr : discr ℚ = 1

Proof state:
b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ discr ℚ = 1

Tactic:
calc NumberField.discr ℚ
  _ = Algebra.discr ℤ b := by convert (discr_eq_discr ℚ b).symm
  _ = Algebra.trace ℤ (𝓞 ℚ) (b default * b default) := by
    rw [Algebra.discr_def, Matrix.det_unique, Algebra.traceMatrix_apply, Algebra.traceForm_apply]
  _ = Algebra.trace ℤ (𝓞 ℚ) 1 := by
    rw [Basis.map_apply, RingEquiv.toAddEquiv_eq_coe, AddEquiv.toIntLinearEquiv_symm,
      AddEquiv.coe_toIntLinearEquiv, Basis.singleton_apply,
      show (AddEquiv.symm ↑ringOfIntegersEquiv) (1 : ℤ) = ringOfIntegersEquiv.symm 1 by rfl,
      map_one, mul_one]
  _ = 1 := by rw [Algebra.trace_eq_matrix_trace b]; norm_num

Result:
no goals

Proof state:
⊢ discr ℚ = 1

Tactic:
let b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
  Basis.map (Basis.singleton (Fin 1) ℤ) ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm

Result:
b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ discr ℚ = 1

Proof state:
b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ discr ℚ = Algebra.discr ℤ ⇑b

Tactic:
convert (discr_eq_discr ℚ b).symm

Result:
no goals

Proof state:
b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ (↑ringOfIntegersEquiv).symm 1 = ringOfIntegersEquiv.symm 1

Tactic:
rfl

Result:
no goals

Proof state:
b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ ((Algebra.leftMulMatrix b) 1).trace = 1

Tactic:
norm_num

Result:
no goals

Proof state:
b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ (Algebra.trace ℤ (𝓞 ℚ)) 1 = 1

Tactic:
rw [Algebra.trace_eq_matrix_trace b]

Result:
b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ ((Algebra.leftMulMatrix b) 1).trace = 1

Proof state:
b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ (Algebra.trace ℤ (𝓞 ℚ)) (b default * b default) = (Algebra.trace ℤ (𝓞 ℚ)) 1

Tactic:
rw [Basis.map_apply, RingEquiv.toAddEquiv_eq_coe, AddEquiv.toIntLinearEquiv_symm,
  AddEquiv.coe_toIntLinearEquiv, Basis.singleton_apply,
  show (AddEquiv.symm ↑ringOfIntegersEquiv) (1 : ℤ) = ringOfIntegersEquiv.symm 1 by rfl,
  map_one, mul_one]

Result:
no goals

Proof state:
b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ Algebra.discr ℤ ⇑b = (Algebra.trace ℤ (𝓞 ℚ)) (b default * b default)

Tactic:
rw [Algebra.discr_def, Matrix.det_unique, Algebra.traceMatrix_apply, Algebra.traceForm_apply]

Result:
no goals
-- Mathlib/NumberTheory/FactorisationProperties.lean
theorem Prime.not_pseudoperfect (h : Prime p) : ¬ Pseudoperfect p

Proof state:
p : ℕ
h : Prime p
⊢ p = 0 ∨ ∀ s ∈ {∅, {1}}, ∑ i ∈ s, i ≠ p

Tactic:
refine Or.inr (fun s hs ↦ ?_)

Result:
p : ℕ
h : Prime p
s : Finset ℕ
hs : s ∈ {∅, {1}}
⊢ ∑ i ∈ s, i ≠ p

Proof state:
p : ℕ
h : Prime p
⊢ {1}.powerset = {∅, {1}}

Tactic:
rfl

Result:
no goals

Proof state:
p : ℕ
h : Prime p
⊢ ¬p.Pseudoperfect

Tactic:
simp_rw [not_pseudoperfect_iff_forall, ← mem_powerset,
  show p.properDivisors.powerset = {∅, {1}} by rw [Prime.properDivisors h]; rfl]

Result:
p : ℕ
h : Prime p
⊢ p = 0 ∨ ∀ s ∈ {∅, {1}}, ∑ i ∈ s, i ≠ p

Proof state:
p : ℕ
h : Prime p
⊢ p.properDivisors.powerset = {∅, {1}}

Tactic:
rw [Prime.properDivisors h]

Result:
p : ℕ
h : Prime p
⊢ {1}.powerset = {∅, {1}}

Proof state:
p : ℕ
h : Prime p
s : Finset ℕ
hs : s ∈ {∅, {1}}
⊢ ∑ i ∈ s, i ≠ p

Tactic:
fin_cases hs <;>
simp only [sum_empty, sum_singleton] <;>
linarith [Prime.one_lt h]

Result:
no goals
-- Mathlib/Data/Multiset/FinsetOps.lean
theorem ndinsert_le {a : α} {s t : Multiset α} : ndinsert a s ≤ t ↔ s ≤ t ∧ a ∈ t :=
  ⟨fun h => ⟨le_trans (le_ndinsert_self _ _) h, mem_of_le h (mem_ndinsert_self _ _)⟩, fun ⟨l, m⟩ =>
    if h : a ∈ s then by simp [h, l]
    else by
      rw [ndinsert_of_not_mem h, ← cons_erase m, cons_le_cons_iff, ← le_cons_of_not_mem h,
          cons_erase m]
      exact l⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
x✝ : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : a ∉ s
⊢ s ≤ t

Tactic:
exact l

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
x✝ : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : a ∉ s
⊢ ndinsert a s ≤ t

Tactic:
rw [ndinsert_of_not_mem h, ← cons_erase m, cons_le_cons_iff, ← le_cons_of_not_mem h,
    cons_erase m]

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
x✝ : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : a ∉ s
⊢ s ≤ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
x✝ : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : a ∈ s
⊢ ndinsert a s ≤ t

Tactic:
simp [h, l]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Grothendieck.lean
theorem superset_covering (Hss : S ≤ R) (sjx : S ∈ J X) : R ∈ J X

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ J X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f R ∈ J Y

Tactic:
apply covering_of_eq_top

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ J X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f R = ⊤

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ J X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f R = ⊤

Tactic:
rw [← top_le_iff, ← S.pullback_eq_top_of_mem hf]

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ J X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f S ≤ Sieve.pullback f R

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ J X
⊢ R ∈ J X

Tactic:
apply J.transitive sjx R fun Y f hf => _

Result:
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ J X
⊢ ∀ (Y : C) (f : Y ⟶ X), S.arrows f → Sieve.pullback f R ∈ J Y

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ J X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f S ≤ Sieve.pullback f R

Tactic:
apply Sieve.pullback_monotone _ Hss

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ J X
⊢ ∀ (Y : C) (f : Y ⟶ X), S.arrows f → Sieve.pullback f R ∈ J Y

Tactic:
intros Y f hf

Result:
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ J X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f R ∈ J Y
-- Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean
/--
Explicit formula for `toCircle j`. Note that this is "evil" because it uses `ZMod.val`. Where
possible, it is recommended to lift `j` to `ℤ` and use `toCircle_intCast` instead.
-/
lemma toCircle_apply (j : ZMod N) :
    toCircle j = exp (2 * π * I * j.val / N)

Proof state:
N : ℕ
inst✝ : NeZero N
j : ZMod N
⊢ ↑(toCircle j) = cexp (2 * ↑π * I * ↑j.val / ↑N)

Tactic:
rw [← toCircle_natCast, natCast_zmod_val]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
lemma arg_lt_pi_div_two_iff {z : ℂ} : arg z < π / 2 ↔ 0 < re z ∨ im z < 0 ∨ z = 0

Proof state:
case inr.inl
z : ℂ
hre : z.re = 0
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
have : z = 0 ↔ z.im = 0 := by simp [Complex.ext_iff, hre]

Result:
case inr.inl
z : ℂ
hre : z.re = 0
this : z = 0 ↔ z.im = 0
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Proof state:
z : ℂ
hre : z.re = 0
⊢ z = 0 ↔ z.im = 0

Tactic:
simp [Complex.ext_iff, hre]

Result:
no goals

Proof state:
case inr.inl
z : ℂ
hre : z.re = 0
this : z = 0 ↔ z.im = 0
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
simp [hre, this, or_comm, le_iff_eq_or_lt]

Result:
no goals

Proof state:
case inl
z : ℂ
hre : z.re < 0
this : z ≠ 0
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
simp [hre.ne, hre.not_le, hre.not_lt, this]

Result:
no goals

Proof state:
case inr.inr
z : ℂ
hre : 0 < z.re
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
simp [hre, hre.le, hre.ne']

Result:
no goals

Proof state:
case inl
z : ℂ
hre : z.re < 0
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
have : z ≠ 0 := by simp [Complex.ext_iff, hre.ne]

Result:
case inl
z : ℂ
hre : z.re < 0
this : z ≠ 0
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Proof state:
z : ℂ
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
rcases lt_trichotomy z.re 0 with hre | hre | hre

Result:
case inl
z : ℂ
hre : z.re < 0
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

case inr.inl
z : ℂ
hre : z.re = 0
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

case inr.inr
z : ℂ
hre : 0 < z.re
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Proof state:
z : ℂ
⊢ z.arg < π / 2 ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
rw [lt_iff_le_and_ne, arg_le_pi_div_two_iff, Ne, arg_eq_pi_div_two_iff]

Result:
z : ℂ
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Proof state:
z : ℂ
hre : z.re < 0
⊢ z ≠ 0

Tactic:
simp [Complex.ext_iff, hre.ne]

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
theorem rel_add_right {as bs₀ bs₁} :
    Rel r as (bs₀ + bs₁) ↔ ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁

Proof state:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ Rel r as (bs₀ + bs₁) ↔ ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁

Tactic:
rw [← rel_flip, rel_add_left]

Result:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ (∃ bs₀_1 bs₁_1, Rel (flip r) bs₀ bs₀_1 ∧ Rel (flip r) bs₁ bs₁_1 ∧ as = bs₀_1 + bs₁_1) ↔
    ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁

Proof state:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ (∃ bs₀_1 bs₁_1, Rel (flip r) bs₀ bs₀_1 ∧ Rel (flip r) bs₁ bs₁_1 ∧ as = bs₀_1 + bs₁_1) ↔
    ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁

Tactic:
simp [rel_flip]

Result:
no goals
-- Mathlib/Computability/TMToPartrec.lean
theorem trStmts₁_trans {q q'} : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q

Proof state:
case read
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
s : Option Γ'
h : q' ∈ trStmts₁ (q s)
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ x ∈ insert (Λ'.read q) (Finset.univ.biUnion fun s => trStmts₁ (q s))

Tactic:
simp only [Finset.mem_biUnion, Finset.mem_univ, true_and, Finset.mem_insert]

Result:
case read
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
s : Option Γ'
h : q' ∈ trStmts₁ (q s)
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ x = Λ'.read q ∨ ∃ a, x ∈ trStmts₁ (q a)

Proof state:
case read
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
⊢ (q' ∈ Finset.univ.biUnion fun s => trStmts₁ (q s)) →
    trStmts₁ q' ⊆ insert (Λ'.read q) (Finset.univ.biUnion fun s => trStmts₁ (q s))

Tactic:
simp

Result:
case read
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
⊢ ∀ (x : Option Γ'),
    q' ∈ trStmts₁ (q x) → trStmts₁ q' ⊆ insert (Λ'.read q) (Finset.univ.biUnion fun s => trStmts₁ (q s))
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma map_genWeightSpace_le :
    (genWeightSpace M χ).map f ≤ genWeightSpace M₂ χ

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
m : M
hm : m ∈ genWeightSpace M χ
x : L
this : ((toEnd R L M₂) x - χ x • 1) ∘ₗ ↑f = ↑f ∘ₗ ((toEnd R L M) x - χ x • 1)
k : ℕ
h : (((toEnd R L M) x - χ x • 1) ^ k) m = 0
⊢ (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0

Tactic:
simpa [h] using LinearMap.congr_fun (LinearMap.commute_pow_left_of_commute this k) m

Result:
no goals

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
m : M
hm : m ∈ genWeightSpace M χ
x : L
this : ((toEnd R L M₂) x - χ x • 1) ∘ₗ ↑f = ↑f ∘ₗ ((toEnd R L M) x - χ x • 1)
⊢ ∃ k, (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0

Tactic:
obtain ⟨k, h⟩ := (mem_genWeightSpace _ _ _).mp hm x

Result:
case intro
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
m : M
hm : m ∈ genWeightSpace M χ
x : L
this : ((toEnd R L M₂) x - χ x • 1) ∘ₗ ↑f = ↑f ∘ₗ ((toEnd R L M) x - χ x • 1)
k : ℕ
h : (((toEnd R L M) x - χ x • 1) ^ k) m = 0
⊢ ∃ k, (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem mem_drop_iff_getElem {l : List α} {a : α} :
    a ∈ l.drop n ↔ ∃ (i : Nat) (hm : i + n < l.length), l[n + i] = a

Proof state:
α : Type u_1
n : Nat
l : List α
i : Nat
hm✝ : i < (drop n l).length
hm : i < l.length - n
⊢ i + n < l.length

Tactic:
omega

Result:
no goals

Proof state:
case mp
α : Type u_1
n : Nat
l : List α
a : α
⊢ (∃ i h, (drop n l)[i] = a) → ∃ i hm, l[n + i] = a

Tactic:
rintro ⟨i, hm, rfl⟩

Result:
case mp.intro.intro
α : Type u_1
n : Nat
l : List α
i : Nat
hm : i < (drop n l).length
⊢ ∃ i_1 hm_1, l[n + i_1] = (drop n l)[i]

Proof state:
case mpr.intro.intro
α : Type u_1
n : Nat
l : List α
i : Nat
hm : i + n < l.length
⊢ ∃ i_1 h, (drop n l)[i_1] = l[n + i]

Tactic:
refine ⟨i, by simp; omega, by rw [getElem_drop]⟩

Result:
no goals

Proof state:
case mp.intro.intro
α : Type u_1
n : Nat
l : List α
i : Nat
hm✝ : i < (drop n l).length
hm : i < l.length - n
⊢ ∃ i_1 hm, l[n + i_1] = (drop n l)[i]

Tactic:
refine ⟨i, by omega, by rw [getElem_drop]⟩

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : List α
i : Nat
hm : i + n < l.length
⊢ (drop n l)[i] = l[n + i]

Tactic:
rw [getElem_drop]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : List α
a : α
⊢ (∃ i h, (drop n l)[i] = a) ↔ ∃ i hm, l[n + i] = a

Tactic:
constructor

Result:
case mp
α : Type u_1
n : Nat
l : List α
a : α
⊢ (∃ i h, (drop n l)[i] = a) → ∃ i hm, l[n + i] = a

case mpr
α : Type u_1
n : Nat
l : List α
a : α
⊢ (∃ i hm, l[n + i] = a) → ∃ i h, (drop n l)[i] = a

Proof state:
α : Type u_1
n : Nat
l : List α
i : Nat
hm✝ : i < (drop n l).length
hm : i < l.length - n
⊢ l[n + i] = (drop n l)[i]

Tactic:
rw [getElem_drop]

Result:
no goals

Proof state:
case mpr
α : Type u_1
n : Nat
l : List α
a : α
⊢ (∃ i hm, l[n + i] = a) → ∃ i h, (drop n l)[i] = a

Tactic:
rintro ⟨i, hm, rfl⟩

Result:
case mpr.intro.intro
α : Type u_1
n : Nat
l : List α
i : Nat
hm : i + n < l.length
⊢ ∃ i_1 h, (drop n l)[i_1] = l[n + i]

Proof state:
α : Type u_1
n : Nat
l : List α
a : α
⊢ a ∈ drop n l ↔ ∃ i hm, l[n + i] = a

Tactic:
rw [mem_iff_getElem]

Result:
α : Type u_1
n : Nat
l : List α
a : α
⊢ (∃ i h, (drop n l)[i] = a) ↔ ∃ i hm, l[n + i] = a

Proof state:
case mp.intro.intro
α : Type u_1
n : Nat
l : List α
i : Nat
hm : i < (drop n l).length
⊢ ∃ i_1 hm_1, l[n + i_1] = (drop n l)[i]

Tactic:
simp at hm

Result:
case mp.intro.intro
α : Type u_1
n : Nat
l : List α
i : Nat
hm✝ : i < (drop n l).length
hm : i < l.length - n
⊢ ∃ i_1 hm, l[n + i_1] = (drop n l)[i]

Proof state:
α : Type u_1
n : Nat
l : List α
i : Nat
hm : i + n < l.length
⊢ i < (drop n l).length

Tactic:
simp

Result:
α : Type u_1
n : Nat
l : List α
i : Nat
hm : i + n < l.length
⊢ i < l.length - n

Proof state:
α : Type u_1
n : Nat
l : List α
i : Nat
hm : i + n < l.length
⊢ i < l.length - n

Tactic:
omega

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_closedBall_mul_of_pos (x : E) {r : ℝ} (hr : 0 < r) (s : ℝ) :
    μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 s)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : 0 < r
s : ℝ
⊢ μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 s)

Tactic:
have : closedBall (0 : E) (r * s) = r • closedBall (0 : E) s := by
  simp [smul_closedBall' hr.ne' (0 : E), abs_of_nonneg hr.le]

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : 0 < r
s : ℝ
this : closedBall 0 (r * s) = r • closedBall 0 s
⊢ μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 s)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : 0 < r
s : ℝ
⊢ closedBall 0 (r * s) = r • closedBall 0 s

Tactic:
simp [smul_closedBall' hr.ne' (0 : E), abs_of_nonneg hr.le]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : 0 < r
s : ℝ
this : closedBall 0 (r * s) = r • closedBall 0 s
⊢ μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 s)

Tactic:
simp only [this, addHaar_smul, abs_of_nonneg hr.le, addHaar_closedBall_center, abs_pow]

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem comp_iff {r : α → Prop → Prop} : r ∘r (· ↔ ·) = r

Proof state:
α : Type u_1
r : α → Prop → Prop
this : (fun x1 x2 => x1 ↔ x2) = fun x1 x2 => x1 = x2
⊢ (r ∘r fun x1 x2 => x1 ↔ x2) = r

Tactic:
rw [this, comp_eq]

Result:
no goals

Proof state:
α : Type u_1
r : α → Prop → Prop
⊢ (fun x1 x2 => x1 ↔ x2) = fun x1 x2 => x1 = x2

Tactic:
funext a b

Result:
case h.h
α : Type u_1
r : α → Prop → Prop
a b : Prop
⊢ (a ↔ b) = (a = b)

Proof state:
case h.h
α : Type u_1
r : α → Prop → Prop
a b : Prop
⊢ (a ↔ b) = (a = b)

Tactic:
exact iff_eq_eq

Result:
no goals