harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/KrullDimension.lean
lemma coheight_le_coheight_apply_of_strictMono (f : α → β) (hf : StrictMono f) (x : α) :
    coheight x ≤ coheight (f x)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
⊢ coheight x ≤ coheight (f x)

Tactic:
apply height_le_height_apply_of_strictMono (α := αᵒᵈ)

Result:
case hf
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
⊢ StrictMono f

Proof state:
case hf
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
⊢ StrictMono f

Tactic:
exact fun _ _ h ↦ hf h

Result:
no goals
-- Mathlib/Data/PNat/Factors.lean
theorem factorMultiset_lcm (m n : ℕ+) :
    factorMultiset (lcm m n) = factorMultiset m ⊔ factorMultiset n

Proof state:
case a
m n : ℕ+
⊢ (m.lcm n).factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset

Tactic:
rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]

Result:
case a
m n : ℕ+
⊢ m.lcm n ∣ (m.factorMultiset ⊔ n.factorMultiset).prod

Proof state:
case a.right
m n : ℕ+
⊢ n ∣ m.lcm n

Tactic:
exact dvd_lcm_right m n

Result:
no goals

Proof state:
case a.hn
m n : ℕ+
⊢ n.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset

Tactic:
exact le_sup_right

Result:
no goals

Proof state:
case a.left
m n : ℕ+
⊢ m ∣ m.lcm n

Tactic:
exact dvd_lcm_left m n

Result:
no goals

Proof state:
m n : ℕ+
⊢ (m.lcm n).factorMultiset = m.factorMultiset ⊔ n.factorMultiset

Tactic:
apply le_antisymm

Result:
case a
m n : ℕ+
⊢ (m.lcm n).factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset

case a
m n : ℕ+
⊢ m.factorMultiset ⊔ n.factorMultiset ≤ (m.lcm n).factorMultiset

Proof state:
case a.hm
m n : ℕ+
⊢ m.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset

Tactic:
exact le_sup_left

Result:
no goals

Proof state:
case a
m n : ℕ+
⊢ m.lcm n ∣ (m.factorMultiset ⊔ n.factorMultiset).prod

Tactic:
apply lcm_dvd <;> rw [← factorMultiset_le_iff']

Result:
case a.hm
m n : ℕ+
⊢ m.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset

case a.hn
m n : ℕ+
⊢ n.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset

Proof state:
case a
m n : ℕ+
⊢ m.factorMultiset ⊔ n.factorMultiset ≤ (m.lcm n).factorMultiset

Tactic:
apply sup_le_iff.mpr

Result:
case a
m n : ℕ+
⊢ m.factorMultiset ≤ (m.lcm n).factorMultiset ∧ n.factorMultiset ≤ (m.lcm n).factorMultiset

Proof state:
case a
m n : ℕ+
⊢ m.factorMultiset ≤ (m.lcm n).factorMultiset ∧ n.factorMultiset ≤ (m.lcm n).factorMultiset

Tactic:
constructor <;> apply factorMultiset_le_iff.mpr

Result:
case a.left
m n : ℕ+
⊢ m ∣ m.lcm n

case a.right
m n : ℕ+
⊢ n ∣ m.lcm n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem any_beq [BEq α] {xs : Vector α n} {a : α} : (xs.any fun x => a == x) = xs.contains a

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a : α
xs : Array α
⊢ ({ toArray := xs, size_toArray := ⋯ }.any fun x => a == x) = { toArray := xs, size_toArray := ⋯ }.contains a

Tactic:
simp [Array.any_beq]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
xs : Vector α n
a : α
⊢ (xs.any fun x => a == x) = xs.contains a

Tactic:
rcases xs with ⟨xs, rfl⟩

Result:
case mk
α : Type u_1
inst✝ : BEq α
a : α
xs : Array α
⊢ ({ toArray := xs, size_toArray := ⋯ }.any fun x => a == x) = { toArray := xs, size_toArray := ⋯ }.contains a
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma genEigenspace_nat {f : End R M} {μ : R} {k : ℕ} :
    f.genEigenspace μ k = LinearMap.ker ((f - μ • 1) ^ k)

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
⊢ (f.genEigenspace μ) ↑k = LinearMap.ker ((f - μ • 1) ^ k)

Tactic:
ext

Result:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x✝ : M
⊢ x✝ ∈ (f.genEigenspace μ) ↑k ↔ x✝ ∈ LinearMap.ker ((f - μ • 1) ^ k)

Proof state:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x✝ : M
⊢ x✝ ∈ (f.genEigenspace μ) ↑k ↔ x✝ ∈ LinearMap.ker ((f - μ • 1) ^ k)

Tactic:
simp [mem_genEigenspace_nat]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Lemmas.lean
theorem cast_inv_nat (n : ℕ) : ((n⁻¹ : ℚ) : α) = (n : α)⁻¹

Proof state:
case zero
α : Type u_1
inst✝ : DivisionRing α
⊢ ↑(↑0)⁻¹ = (↑0)⁻¹

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(n + 1))⁻¹ = (↑(n + 1))⁻¹

Tactic:
rw [cast_def, inv_natCast_num, inv_natCast_den, if_neg n.succ_ne_zero,
  Int.sign_eq_one_of_pos (Int.ofNat_succ_pos n), Int.cast_one, one_div]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑n)⁻¹ = (↑n)⁻¹

Tactic:
rcases n with - | n

Result:
case zero
α : Type u_1
inst✝ : DivisionRing α
⊢ ↑(↑0)⁻¹ = (↑0)⁻¹

case succ
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(n + 1))⁻¹ = (↑(n + 1))⁻¹
-- Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean
theorem contDiffOn_succ_iff_fderiv_apply [FiniteDimensional 𝕜 D] (hs : UniqueDiffOn 𝕜 s) :
    ContDiffOn 𝕜 (n + 1) f s ↔
      DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧
      ∀ y, ContDiffOn 𝕜 n (fun x => fderivWithin 𝕜 f s x y) s

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace 𝕜 D
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : WithTop ℕ∞
f : D → E
s : Set D
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 D
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 (n + 1) f s ↔
    DifferentiableOn 𝕜 f s ∧
      (n = ω → AnalyticOn 𝕜 f s) ∧ ∀ (y : D), ContDiffOn 𝕜 n (fun x => (fderivWithin 𝕜 f s x) y) s

Tactic:
rw [contDiffOn_succ_iff_fderivWithin hs, contDiffOn_clm_apply]

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem testBit_bit_zero (b) : ∀ n, testBit (bit b n) 0 = b
  | (n : ℕ) => by rw [bit_coe_nat]; apply Nat.testBit_bit_zero
  | -[n+1] => by
    rw [bit_negSucc]; dsimp [testBit]; rw [Nat.testBit_bit_zero]; clear testBit_bit_zero
    cases b <;>
      rfl

Proof state:
b : Bool
n : ℕ
⊢ (bit b -[n+1]).testBit 0 = b

Tactic:
rw [bit_negSucc]

Result:
b : Bool
n : ℕ
⊢ -[Nat.bit (!b) n+1].testBit 0 = b

Proof state:
b : Bool
n : ℕ
⊢ (!!b) = b

Tactic:
cases b <;>
  rfl

Result:
no goals

Proof state:
b : Bool
n : ℕ
⊢ (!(Nat.bit (!b) n).testBit 0) = b

Tactic:
rw [Nat.testBit_bit_zero]

Result:
b : Bool
n : ℕ
⊢ (!!b) = b

Proof state:
b : Bool
n : ℕ
⊢ (↑(Nat.bit b n)).testBit 0 = b

Tactic:
apply Nat.testBit_bit_zero

Result:
no goals

Proof state:
b : Bool
n : ℕ
⊢ (bit b ↑n).testBit 0 = b

Tactic:
rw [bit_coe_nat]

Result:
b : Bool
n : ℕ
⊢ (↑(Nat.bit b n)).testBit 0 = b

Proof state:
b : Bool
n : ℕ
⊢ -[Nat.bit (!b) n+1].testBit 0 = b

Tactic:
dsimp [testBit]

Result:
b : Bool
n : ℕ
⊢ (!(Nat.bit (!b) n).testBit 0) = b
-- Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
theorem MultilinearMap.domCoprod_alternization [DecidableEq ιa] [DecidableEq ιb]
    (a : MultilinearMap R' (fun _ : ιa => Mᵢ) N₁) (b : MultilinearMap R' (fun _ : ιb => Mᵢ) N₂) :
    MultilinearMap.alternatization (MultilinearMap.domCoprod a b) =
      a.alternatization.domCoprod (MultilinearMap.alternatization b)

Proof state:
case a.e_f.h.e_f.h.mk
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x => Mᵢ) N₁
b : MultilinearMap R' (fun x => Mᵢ) N₂
σ✝ : Quotient (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)
σ : Perm (ιa ⊕ ιb)
al : Perm ιa
ar : Perm ιb
⊢ Perm.sign (σ * (Perm.sumCongrHom ιa ιb) (al, ar)) •
      domDomCongr (σ * (Perm.sumCongrHom ιa ιb) (al, ar)) (a.domCoprod b) =
    Perm.sign σ • Perm.sign al • Perm.sign ar • domDomCongr σ ((domDomCongr al a).domCoprod (domDomCongr ar b))

Tactic:
rw [MultilinearMap.domDomCongr_mul, Perm.sign_mul, Perm.sumCongrHom_apply,
  MultilinearMap.domCoprod_domDomCongr_sumCongr, Perm.sign_sumCongr, mul_smul, mul_smul]

Result:
no goals
-- Mathlib/Algebra/Lie/Solvable.lean
theorem solvable_iff_equiv_solvable (e : L' ≃ₗ⁅R⁆ L) : IsSolvable L' ↔ IsSolvable L

Proof state:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L' ≃ₗ⁅R⁆ L
⊢ IsSolvable L' ↔ IsSolvable L

Tactic:
constructor <;> intro h

Result:
case mp
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L' ≃ₗ⁅R⁆ L
h : IsSolvable L'
⊢ IsSolvable L

case mpr
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L' ≃ₗ⁅R⁆ L
h : IsSolvable L
⊢ IsSolvable L'

Proof state:
case mp
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L' ≃ₗ⁅R⁆ L
h : IsSolvable L'
⊢ IsSolvable L

Tactic:
exact e.symm.injective.lieAlgebra_isSolvable

Result:
no goals

Proof state:
case mpr
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L' ≃ₗ⁅R⁆ L
h : IsSolvable L
⊢ IsSolvable L'

Tactic:
exact e.injective.lieAlgebra_isSolvable

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.filterMap (f : α → Option β) {l₁ l₂ : List α} (p : l₁ ~ l₂) :
    filterMap f l₁ ~ filterMap f l₂

Proof state:
case swap
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂✝ : List α
x y : α
l₂ : List α
⊢ List.filterMap f (y :: x :: l₂) ~ List.filterMap f (x :: y :: l₂)

Tactic:
cases hx : f x <;> cases hy : f y <;> simp [hx, hy, filterMap_cons, swap]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ : List α
x : α
l₁✝ l₂✝ : List α
_p : l₁✝ ~ l₂✝
IH : List.filterMap f l₁✝ ~ List.filterMap f l₂✝
⊢ List.filterMap f (x :: l₁✝) ~ List.filterMap f (x :: l₂✝)

Tactic:
cases h : f x <;> simp [h, filterMap_cons, IH, Perm.cons]

Result:
no goals

Proof state:
case trans
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
_p₁ : l₁✝ ~ l₂✝
_p₂ : l₂✝ ~ l₃✝
IH₁ : List.filterMap f l₁✝ ~ List.filterMap f l₂✝
IH₂ : List.filterMap f l₂✝ ~ List.filterMap f l₃✝
⊢ List.filterMap f l₁✝ ~ List.filterMap f l₃✝

Tactic:
exact IH₁.trans IH₂

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ : List α
⊢ List.filterMap f [] ~ List.filterMap f []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ List.filterMap f l₁ ~ List.filterMap f l₂

Tactic:
induction p with
| nil => simp
| cons x _p IH => cases h : f x <;> simp [h, filterMap_cons, IH, Perm.cons]
| swap x y l₂ => cases hx : f x <;> cases hy : f y <;> simp [hx, hy, filterMap_cons, swap]
| trans _p₁ _p₂ IH₁ IH₂ => exact IH₁.trans IH₂

Result:
no goals
-- Mathlib/Analysis/Complex/Basic.lean
theorem nnnorm_eq_one_of_pow_eq_one {ζ : ℂ} {n : ℕ} (h : ζ ^ n = 1) (hn : n ≠ 0) : ‖ζ‖₊ = 1 :=
  (pow_left_inj₀ zero_le' zero_le' hn).1 <| by rw [← nnnorm_pow, h, nnnorm_one, one_pow]

Proof state:
ζ : ℂ
n : ℕ
h : ζ ^ n = 1
hn : n ≠ 0
⊢ ‖ζ‖₊ ^ n = 1 ^ n

Tactic:
rw [← nnnorm_pow, h, nnnorm_one, one_pow]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/ConformalLinearMap.lean
theorem ne_zero [Nontrivial M'] {f' : M' →L[R] N} (hf' : IsConformalMap f') : f' ≠ 0

Proof state:
R : Type u_1
N : Type u_3
M' : Type u_5
inst✝⁵ : NormedField R
inst✝⁴ : SeminormedAddCommGroup N
inst✝³ : NormedSpace R N
inst✝² : NormedAddCommGroup M'
inst✝¹ : NormedSpace R M'
inst✝ : Nontrivial M'
hf' : IsConformalMap 0
⊢ False

Tactic:
rcases exists_ne (0 : M') with ⟨a, ha⟩

Result:
case intro
R : Type u_1
N : Type u_3
M' : Type u_5
inst✝⁵ : NormedField R
inst✝⁴ : SeminormedAddCommGroup N
inst✝³ : NormedSpace R N
inst✝² : NormedAddCommGroup M'
inst✝¹ : NormedSpace R M'
inst✝ : Nontrivial M'
hf' : IsConformalMap 0
a : M'
ha : a ≠ 0
⊢ False

Proof state:
case intro
R : Type u_1
N : Type u_3
M' : Type u_5
inst✝⁵ : NormedField R
inst✝⁴ : SeminormedAddCommGroup N
inst✝³ : NormedSpace R N
inst✝² : NormedAddCommGroup M'
inst✝¹ : NormedSpace R M'
inst✝ : Nontrivial M'
hf' : IsConformalMap 0
a : M'
ha : a ≠ 0
⊢ False

Tactic:
exact ha (hf'.injective rfl)

Result:
no goals

Proof state:
R : Type u_1
N : Type u_3
M' : Type u_5
inst✝⁵ : NormedField R
inst✝⁴ : SeminormedAddCommGroup N
inst✝³ : NormedSpace R N
inst✝² : NormedAddCommGroup M'
inst✝¹ : NormedSpace R M'
inst✝ : Nontrivial M'
f' : M' →L[R] N
hf' : IsConformalMap f'
⊢ f' ≠ 0

Tactic:
rintro rfl

Result:
R : Type u_1
N : Type u_3
M' : Type u_5
inst✝⁵ : NormedField R
inst✝⁴ : SeminormedAddCommGroup N
inst✝³ : NormedSpace R N
inst✝² : NormedAddCommGroup M'
inst✝¹ : NormedSpace R M'
inst✝ : Nontrivial M'
hf' : IsConformalMap 0
⊢ False
-- Mathlib/Algebra/BigOperators/Ring/Nat.lean
lemma even_sum_iff_even_card_odd {s : Finset ι} (f : ι → ℕ) :
    Even (∑ i ∈ s, f i) ↔ Even (s.filter fun x ↦ Odd (f x)).card

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ Even (∑ i ∈ s, f i) ↔ Even #(filter (fun x => Odd (f x)) s)

Tactic:
rw [← Finset.sum_filter_add_sum_filter_not _ (fun x ↦ Even (f x)), Nat.even_add]

Result:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (Even (∑ x ∈ filter (fun x => Even (f x)) s, f x) ↔ Even (∑ x ∈ filter (fun x => ¬Even (f x)) s, f x)) ↔
    Even #(filter (fun x => Odd (f x)) s)

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ Even (∑ x ∈ filter (fun x => ¬Even (f x)) s, f x) ↔ Even #(filter (fun x => Odd (f x)) s)

Tactic:
rw [Nat.even_iff, Finset.sum_nat_mod, Finset.sum_filter]

Result:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (∑ a ∈ s, if ¬Even (f a) then f a % 2 else 0) % 2 = 0 ↔ Even #(filter (fun x => Odd (f x)) s)

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (Even (∑ x ∈ filter (fun x => Even (f x)) s, f x) ↔ Even (∑ x ∈ filter (fun x => ¬Even (f x)) s, f x)) ↔
    Even #(filter (fun x => Odd (f x)) s)

Tactic:
simp only [Finset.mem_filter, and_imp, imp_self, implies_true, Finset.even_sum, true_iff]

Result:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ Even (∑ x ∈ filter (fun x => ¬Even (f x)) s, f x) ↔ Even #(filter (fun x => Odd (f x)) s)

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (∑ x ∈ s, if Odd (f x) then 1 else 0) % 2 = 0 ↔ Even #(filter (fun x => Odd (f x)) s)

Tactic:
simp_rw [← Finset.sum_filter, ← Nat.even_iff, Finset.card_eq_sum_ones]

Result:
no goals

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (∑ a ∈ s, if ¬Even (f a) then f a % 2 else 0) % 2 = 0 ↔ Even #(filter (fun x => Odd (f x)) s)

Tactic:
simp +contextual only [Nat.not_even_iff_odd, Nat.odd_iff.mp]

Result:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (∑ x ∈ s, if Odd (f x) then 1 else 0) % 2 = 0 ↔ Even #(filter (fun x => Odd (f x)) s)
-- Mathlib/Data/Nat/Init.lean
lemma le_self_pow (hn : n ≠ 0) : ∀ a : ℕ, a ≤ a ^ n
  | 0 => zero_le _
  | a + 1 => by simpa using Nat.pow_le_pow_right a.succ_pos (Nat.one_le_iff_ne_zero.2 hn)

Proof state:
n : ℕ
hn : n ≠ 0
a : ℕ
⊢ a + 1 ≤ (a + 1) ^ n

Tactic:
simpa using Nat.pow_le_pow_right a.succ_pos (Nat.one_le_iff_ne_zero.2 hn)

Result:
no goals
-- Mathlib/Algebra/Lie/Normalizer.lean
theorem normalizer_eq_self_iff :
    H.normalizer = H ↔ (LieModule.maxTrivSubmodule R H <| L ⧸ H.toLieSubmodule) = ⊥

Proof state:
case refine_1
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
⊢ ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0

Tactic:
rintro ⟨x⟩ hx

Result:
case refine_1.mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x : L
hx : Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
⊢ Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x = 0

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
⊢ H.normalizer = H ↔ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule) = ⊥

Tactic:
rw [LieSubmodule.eq_bot_iff]

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
⊢ H.normalizer = H ↔ ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0

Proof state:
case refine_2
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
x : L
hx : x ∈ H.normalizer
y : L ⧸ H.toLieSubmodule := (LieSubmodule.Quotient.mk' H.toLieSubmodule) x
⊢ x ∈ H

Tactic:
have hy : y ∈ LieModule.maxTrivSubmodule R H (L ⧸ H.toLieSubmodule) := by
  rintro ⟨z, hz⟩
  rw [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero, coe_bracket_of_module,
    Submodule.coe_mk, mem_toLieSubmodule]
  exact (H.mem_normalizer_iff' x).mp hx z hz

Result:
case refine_2
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
x : L
hx : x ∈ H.normalizer
y : L ⧸ H.toLieSubmodule := (LieSubmodule.Quotient.mk' H.toLieSubmodule) x
hy : y ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
⊢ x ∈ H

Proof state:
case refine_2
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
⊢ H.normalizer ≤ H

Tactic:
intro x hx

Result:
case refine_2
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
x : L
hx : x ∈ H.normalizer
⊢ x ∈ H
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousOn_iff_continuous_restrict :
    ContinuousOn f s ↔ Continuous (s.restrict f)

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) → ∀ (x : ↑s), ContinuousAt (s.restrict f) x

Tactic:
rintro h ⟨x, xs⟩

Result:
case mp.mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ContinuousWithinAt f s x
x : α
xs : x ∈ s
⊢ ContinuousAt (s.restrict f) ⟨x, xs⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ Continuous (s.restrict f)

Tactic:
rw [ContinuousOn, continuous_iff_continuousAt]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) ↔ ∀ (x : ↑s), ContinuousAt (s.restrict f) x

Proof state:
case mp.mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ContinuousWithinAt f s x
x : α
xs : x ∈ s
⊢ ContinuousAt (s.restrict f) ⟨x, xs⟩

Tactic:
exact (continuousWithinAt_iff_continuousAt_restrict f xs).mp (h x xs)

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ (x : ↑s), ContinuousAt (s.restrict f) x
x : α
xs : x ∈ s
⊢ ContinuousWithinAt f s x

Tactic:
exact (continuousWithinAt_iff_continuousAt_restrict f xs).mpr (h ⟨x, xs⟩)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) ↔ ∀ (x : ↑s), ContinuousAt (s.restrict f) x

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) → ∀ (x : ↑s), ContinuousAt (s.restrict f) x

case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ (∀ (x : ↑s), ContinuousAt (s.restrict f) x) → ∀ x ∈ s, ContinuousWithinAt f s x

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ (∀ (x : ↑s), ContinuousAt (s.restrict f) x) → ∀ x ∈ s, ContinuousWithinAt f s x

Tactic:
intro h x xs

Result:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ (x : ↑s), ContinuousAt (s.restrict f) x
x : α
xs : x ∈ s
⊢ ContinuousWithinAt f s x
-- Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
theorem norm_iteratedFDeriv_clm_apply {f : E → F →L[𝕜] G} {g : E → F} {N : WithTop ℕ∞} {n : ℕ}
    (hf : ContDiff 𝕜 N f) (hg : ContDiff 𝕜 N g) (x : E) (hn : n ≤ N) :
    ‖iteratedFDeriv 𝕜 n (fun y : E => (f y) (g y)) x‖ ≤ ∑ i ∈ Finset.range (n + 1),
      ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
g : E → F
N : WithTop ℕ∞
n : ℕ
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : E
hn : ↑n ≤ N
⊢ ‖iteratedFDeriv 𝕜 n (fun y => (f y) (g y)) x‖ ≤
    ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖

Tactic:
simp only [← iteratedFDerivWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
g : E → F
N : WithTop ℕ∞
n : ℕ
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : E
hn : ↑n ≤ N
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y => (f y) (g y)) univ x‖ ≤
    ∑ x_1 ∈ Finset.range (n + 1),
      ↑(n.choose x_1) * ‖iteratedFDerivWithin 𝕜 x_1 f univ x‖ * ‖iteratedFDerivWithin 𝕜 (n - x_1) g univ x‖

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
g : E → F
N : WithTop ℕ∞
n : ℕ
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : E
hn : ↑n ≤ N
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y => (f y) (g y)) univ x‖ ≤
    ∑ x_1 ∈ Finset.range (n + 1),
      ↑(n.choose x_1) * ‖iteratedFDerivWithin 𝕜 x_1 f univ x‖ * ‖iteratedFDerivWithin 𝕜 (n - x_1) g univ x‖

Tactic:
exact norm_iteratedFDerivWithin_clm_apply hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ
  (Set.mem_univ x) hn

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem continuousAt_const_rpow' {a b : ℝ} (h : b ≠ 0) : ContinuousAt (a ^ ·) b

Proof state:
a b : ℝ
h : b ≠ 0
⊢ ↑b ≠ 0

Tactic:
norm_cast

Result:
no goals

Proof state:
a b : ℝ
h : b ≠ 0
⊢ ContinuousAt (fun x => ↑a ^ ↑x) b

Tactic:
refine (continuousAt_const_cpow' ?_).comp Complex.continuous_ofReal.continuousAt

Result:
a b : ℝ
h : b ≠ 0
⊢ ↑b ≠ 0

Proof state:
a b : ℝ
h : b ≠ 0
⊢ ContinuousAt (fun x => a ^ x) b

Tactic:
simp only [rpow_def]

Result:
a b : ℝ
h : b ≠ 0
⊢ ContinuousAt (fun x => (↑a ^ ↑x).re) b

Proof state:
a b : ℝ
h : b ≠ 0
⊢ ContinuousAt (fun x => (↑a ^ ↑x).re) b

Tactic:
refine Complex.continuous_re.continuousAt.comp ?_

Result:
a b : ℝ
h : b ≠ 0
⊢ ContinuousAt (fun x => ↑a ^ ↑x) b