harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem normalClosure_eq_top_of {N : Subgroup G} [hn : N.Normal] {g g' : G} {hg : g ∈ N}
    {hg' : g' ∈ N} (hc : IsConj g g') (ht : normalClosure ({⟨g, hg⟩} : Set N) = ⊤) :
    normalClosure ({⟨g', hg'⟩} : Set N) = ⊤

Proof state:
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g g' : G
hg : g ∈ N
hg' : g' ∈ N
hc : IsConj g g'
ht : normalClosure {⟨g, hg⟩} = ⊤
⊢ normalClosure {⟨g', hg'⟩} = ⊤

Tactic:
obtain ⟨c, rfl⟩ := isConj_iff.1 hc

Result:
case intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
⊢ normalClosure {⟨c * g * c⁻¹, hg'⟩} = ⊤

Proof state:
case intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
⊢ normalClosure {⟨c * g * c⁻¹, hg'⟩} = ⊤

Tactic:
have h : ∀ x : N, (MulAut.conj c) x ∈ N := by
  rintro ⟨x, hx⟩
  exact hn.conj_mem _ hx c

Result:
case intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
⊢ normalClosure {⟨c * g * c⁻¹, hg'⟩} = ⊤

Proof state:
case mk.refine_2
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ (((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h) ⟨c⁻¹ * x * c, ⋯⟩ = ⟨x, hx⟩

Tactic:
simp only [MonoidHom.codRestrict_apply, MulEquiv.coe_toMonoidHom, MulAut.conj_apply, coe_mk,
  MonoidHom.restrict_apply, Subtype.mk_eq_mk, ← mul_assoc, mul_inv_cancel, one_mul]

Result:
case mk.refine_2
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ x * c * c⁻¹ = x

Proof state:
case intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h)
⊢ ⟨c * g * c⁻¹, ⋯⟩ ∈ normalClosure {⟨c * g * c⁻¹, hg'⟩}

Tactic:
exact subset_normalClosure (Set.mem_singleton _)

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem HasFTaylorSeriesUpToOn.compContinuousLinearMap
    (hf : HasFTaylorSeriesUpToOn n f p s) (g : G →L[𝕜] E) :
    HasFTaylorSeriesUpToOn n (f ∘ g) (fun x k => (p (g x) k).compContinuousLinearMap fun _ => g)
      (g ⁻¹' s)

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
s : Set E
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →L[𝕜] E
⊢ HasFTaylorSeriesUpToOn n (f ∘ ⇑g) (fun x k => (p (g x) k).compContinuousLinearMap fun x => g) (⇑g ⁻¹' s)

Tactic:
let A : ∀ m : ℕ, (E[×m]→L[𝕜] F) → G[×m]→L[𝕜] F := fun m h => h.compContinuousLinearMap fun _ => g

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
s : Set E
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →L[𝕜] E
A : (m : ℕ) → ContinuousMultilinearMap 𝕜 (fun i => E) F → ContinuousMultilinearMap 𝕜 (fun i => G) F :=
  fun m h => h.compContinuousLinearMap fun x => g
⊢ HasFTaylorSeriesUpToOn n (f ∘ ⇑g) (fun x k => (p (g x) k).compContinuousLinearMap fun x => g) (⇑g ⁻¹' s)

Proof state:
case zero_eq
𝕜 : 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
s : Set E
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →L[𝕜] E
A : (m : ℕ) → ContinuousMultilinearMap 𝕜 (fun i => E) F → ContinuousMultilinearMap 𝕜 (fun i => G) F :=
  fun m h => h.compContinuousLinearMap fun x => g
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
x : G
hx : x ∈ ⇑g ⁻¹' s
⊢ ((p (g x) 0) fun x => 0) = (p (g x) 0) 0

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem power_nat_le_max {c : Cardinal.{u}} {n : ℕ} : c ^ (n : Cardinal.{u}) ≤ max c ℵ₀

Proof state:
c : Cardinal.{u}
n : ℕ
⊢ c ^ ↑n ≤ c ⊔ ℵ₀

Tactic:
rcases le_or_lt ℵ₀ c with hc | hc

Result:
case inl
c : Cardinal.{u}
n : ℕ
hc : ℵ₀ ≤ c
⊢ c ^ ↑n ≤ c ⊔ ℵ₀

case inr
c : Cardinal.{u}
n : ℕ
hc : c < ℵ₀
⊢ c ^ ↑n ≤ c ⊔ ℵ₀

Proof state:
case inr
c : Cardinal.{u}
n : ℕ
hc : c < ℵ₀
⊢ c ^ ↑n ≤ c ⊔ ℵ₀

Tactic:
exact le_max_of_le_right (power_lt_aleph0 hc (nat_lt_aleph0 _)).le

Result:
no goals

Proof state:
case inl
c : Cardinal.{u}
n : ℕ
hc : ℵ₀ ≤ c
⊢ c ^ ↑n ≤ c ⊔ ℵ₀

Tactic:
exact le_max_of_le_left (power_nat_le hc)

Result:
no goals
-- Mathlib/Data/Real/Pi/Bounds.lean
theorem pi_gt_d20 : 3.14159265358979323846 < π

Proof state:
⊢ 3.14159265358979323846 < π

Tactic:
pi_lower_bound [
  671574048197/474874563549, 58134718954/31462283181, 3090459598621/1575502640777,
  2-7143849599/741790664068, 8431536490061/4220852446654, 2-2725579171/4524814682468,
  2-2494895647/16566776788806, 2-608997841/16175484287402, 2-942567063/100141194694075,
  2-341084060/144951150987041, 2-213717653/363295959742218, 2-71906926/488934711121807,
  2-29337101/797916288104986, 2-45326311/4931175952730065, 2-7506877/3266776448781479,
  2-5854787/10191338039232571, 2-4538642/31601378399861717, 2-276149/7691013341581098,
  2-350197/39013283396653714, 2-442757/197299283738495963, 2-632505/1127415566199968707,
  2-1157/8249230030392285, 2-205461/5859619883403334178, 2-33721/3846807755987625852,
  2-11654/5317837263222296743, 2-8162/14897610345776687857, 2-731/5337002285107943372,
  2-1320/38549072592845336201, 2-707/82588467645883795866, 2-53/24764858756615791675,
  2-237/442963888703240952920, 2-128/956951523274512100791, 2-32/956951523274512100783,
  2-27/3229711391051478340136]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n)
    (units : Array (Literal (PosFin n))) (units_nodup : ∀ i : Fin units.size, ∀ j : Fin units.size, i ≠ j → units[i] ≠ units[j])
    (idx : Fin units.size) (assignments : Array Assignment)
    (ih : ClearInsertInductionMotive f f_assignments_size units idx.1 assignments) :
    ClearInsertInductionMotive f f_assignments_size units (idx.1 + 1) (clearUnit assignments units[idx])

Proof state:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
⊢ ↑i < assignments.size

Tactic:
rw [hsize]

Result:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
⊢ ↑i < n

Proof state:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_ne_j2 : ¬idx = j2
h1 : units[↑idx].fst.val = ↑i
h2 : units[↑idx].snd = true
h3 : ¬units[↑idx] = (⟨units[↑idx].fst.val, ⋯⟩, units[↑idx].snd)
⊢ False

Tactic:
exact h3 rfl

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem min?_eq_toList_head? {t : RBNode α} : t.min? = t.toList.head?

Proof state:
case nil
α : Type u_1
⊢ nil.min? = nil.toList.head?

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
t : RBNode α
⊢ t.min? = t.toList.head?

Tactic:
induction t with
| nil => rfl
| node _ l _ _ ih =>
  cases l <;> simp [RBNode.min?, ih]

Result:
no goals

Proof state:
case node
α : Type u_1
c✝ : RBColor
l : RBNode α
v✝ : α
r✝ : RBNode α
ih : l.min? = l.toList.head?
r_ih✝ : r✝.min? = r✝.toList.head?
⊢ (node c✝ l v✝ r✝).min? = (node c✝ l v✝ r✝).toList.head?

Tactic:
cases l <;> simp [RBNode.min?, ih]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem toOrdinal_cast_nat (n : ℕ) : toOrdinal n = n

Proof state:
case succ
n : ℕ
hn : toOrdinal ↑n = ↑n
⊢ toOrdinal ↑(n + 1) = ↑(n + 1)

Tactic:
change (toOrdinal n) ♯ 1 = n + 1

Result:
case succ
n : ℕ
hn : toOrdinal ↑n = ↑n
⊢ toOrdinal ↑n ♯ 1 = ↑n + 1

Proof state:
case succ
n : ℕ
hn : toOrdinal ↑n = ↑n
⊢ ↑n ♯ 1 = ↑n + 1

Tactic:
exact nadd_one n

Result:
no goals

Proof state:
case succ
n : ℕ
hn : toOrdinal ↑n = ↑n
⊢ toOrdinal ↑n ♯ 1 = ↑n + 1

Tactic:
rw [hn]

Result:
case succ
n : ℕ
hn : toOrdinal ↑n = ↑n
⊢ ↑n ♯ 1 = ↑n + 1

Proof state:
case zero

⊢ toOrdinal ↑0 = ↑0

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ toOrdinal ↑n = ↑n

Tactic:
induction' n with n hn

Result:
case zero

⊢ toOrdinal ↑0 = ↑0

case succ
n : ℕ
hn : toOrdinal ↑n = ↑n
⊢ toOrdinal ↑(n + 1) = ↑(n + 1)
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_const' [CompleteSpace E] (c : E) :
    ∫ _ in a..b, c ∂μ = ((μ <| Ioc a b).toReal - (μ <| Ioc b a).toReal) • c

Proof state:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
inst✝ : CompleteSpace E
c : E
⊢ ∫ (x : ℝ) in a..b, c ∂μ = ((μ (Ioc a b)).toReal - (μ (Ioc b a)).toReal) • c

Tactic:
simp only [intervalIntegral, setIntegral_const, sub_smul]

Result:
no goals
-- Mathlib/RingTheory/NoetherNormalization.lean
private lemma sum_r_mul_neq (vlt : ∀ i, v i < up) (wlt : ∀ i, w i < up) (neq : v ≠ w) :
    ∑ x : Fin (n + 1), r x * v x ≠ ∑ x : Fin (n + 1), r x * w x

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), v i < up
wlt : ∀ (i : Fin (n + 1)), w i < up
neq : v ≠ w
⊢ ∑ x : Fin (n + 1), r x * v x ≠ ∑ x : Fin (n + 1), r x * w x

Tactic:
intro h

Result:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), v i < up
wlt : ∀ (i : Fin (n + 1)), w i < up
neq : v ≠ w
h : ∑ x : Fin (n + 1), r x * v x = ∑ x : Fin (n + 1), r x * w x
⊢ False

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), v i < up
wlt : ∀ (i : Fin (n + 1)), w i < up
neq : v ≠ w
h : ∑ x : Fin (n + 1), r x * v x = ∑ x : Fin (n + 1), r x * w x
⊢ ofFn ⇑v = ofFn ⇑w

Tactic:
apply ofDigits_inj_of_len_eq (Nat.lt_add_right f.totalDegree one_lt_two)
  (by simp) (lt_up vlt) (lt_up wlt)

Result:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), v i < up
wlt : ∀ (i : Fin (n + 1)), w i < up
neq : v ≠ w
h : ∑ x : Fin (n + 1), r x * v x = ∑ x : Fin (n + 1), r x * w x
⊢ ofDigits up (ofFn ⇑v) = ofDigits up (ofFn ⇑w)

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), v i < up
wlt : ∀ (i : Fin (n + 1)), w i < up
neq : v ≠ w
h : ∑ x : Fin (n + 1), r x * v x = ∑ x : Fin (n + 1), r x * w x
⊢ False

Tactic:
refine neq <| Finsupp.ext <| congrFun <| ofFn_inj.mp ?_

Result:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), v i < up
wlt : ∀ (i : Fin (n + 1)), w i < up
neq : v ≠ w
h : ∑ x : Fin (n + 1), r x * v x = ∑ x : Fin (n + 1), r x * w x
⊢ ofFn ⇑v = ofFn ⇑w

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), v i < up
wlt : ∀ (i : Fin (n + 1)), w i < up
neq : v ≠ w
h : ∑ x : Fin (n + 1), r x * v x = ∑ x : Fin (n + 1), r x * w x
⊢ (ofFn ⇑v).length = (ofFn ⇑w).length

Tactic:
simp

Result:
no goals

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), v i < up
wlt : ∀ (i : Fin (n + 1)), w i < up
neq : v ≠ w
h : ∑ x : Fin (n + 1), r x * v x = ∑ x : Fin (n + 1), r x * w x
⊢ ofDigits up (ofFn ⇑v) = ofDigits up (ofFn ⇑w)

Tactic:
simpa only [ofDigits_eq_sum_mapIdx, mapIdx_eq_ofFn, get_ofFn, length_ofFn,
  Fin.coe_cast, mul_comm, sum_ofFn] using h

Result:
no goals
-- Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
theorem eq_unit_mul_pow_irreducible {x : R} (hx : x ≠ 0) {ϖ : R} (hirr : Irreducible ϖ) :
    ∃ (n : ℕ) (u : Rˣ), x = u * ϖ ^ n

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
n : ℕ
u : Rˣ
hx : ϖ ^ n * ↑u ≠ 0
hn : Associated (ϖ ^ n * ↑u) (ϖ ^ n)
⊢ ϖ ^ n * ↑u = ↑u * ϖ ^ n

Tactic:
apply mul_comm

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
n : ℕ
hn : Associated x (ϖ ^ n)
⊢ ∃ n u, x = ↑u * ϖ ^ n

Tactic:
obtain ⟨u, rfl⟩ := hn.symm

Result:
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
n : ℕ
u : Rˣ
hx : ϖ ^ n * ↑u ≠ 0
hn : Associated (ϖ ^ n * ↑u) (ϖ ^ n)
⊢ ∃ n_1 u_1, ϖ ^ n * ↑u = ↑u_1 * ϖ ^ n_1

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
n : ℕ
u : Rˣ
hx : ϖ ^ n * ↑u ≠ 0
hn : Associated (ϖ ^ n * ↑u) (ϖ ^ n)
⊢ ∃ n_1 u_1, ϖ ^ n * ↑u = ↑u_1 * ϖ ^ n_1

Tactic:
use n, u

Result:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
n : ℕ
u : Rˣ
hx : ϖ ^ n * ↑u ≠ 0
hn : Associated (ϖ ^ n * ↑u) (ϖ ^ n)
⊢ ϖ ^ n * ↑u = ↑u * ϖ ^ n

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
⊢ ∃ n u, x = ↑u * ϖ ^ n

Tactic:
obtain ⟨n, hn⟩ := associated_pow_irreducible hx hirr

Result:
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
n : ℕ
hn : Associated x (ϖ ^ n)
⊢ ∃ n u, x = ↑u * ϖ ^ n
-- Mathlib/MeasureTheory/Measure/OpenPos.lean
theorem _root_.IsClosed.ae_eq_univ_iff_eq (hF : IsClosed F) :
    F =ᵐ[μ] univ ↔ F = univ

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
F : Set X
hF : IsClosed F
h : F = univ
⊢ F =ᶠ[ae μ] univ

Tactic:
rw [h]

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
F : Set X
hF : IsClosed F
h : F =ᶠ[ae μ] univ
⊢ F = univ

Tactic:
rwa [ae_eq_univ, hF.isOpen_compl.measure_eq_zero_iff μ, compl_empty_iff] at h

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
F : Set X
hF : IsClosed F
⊢ F =ᶠ[ae μ] univ ↔ F = univ

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
F : Set X
hF : IsClosed F
h : F =ᶠ[ae μ] univ
⊢ F = univ
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem IsPartition.exists_splitMany_le {I : Box ι} {π : Prepartition I} (h : IsPartition π) :
    ∃ s, splitMany I s ≤ π

Proof state:
ι : Type u_1
inst✝ : Finite ι
I : Box ι
π : Prepartition I
h : π.IsPartition
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = (splitMany I s).filter fun J => ↑J ⊆ π.iUnion
⊢ splitMany I s ≤ π

Tactic:
rwa [h.iUnion_eq, filter_of_true, inf_eq_right] at hs

Result:
case hp
ι : Type u_1
inst✝ : Finite ι
I : Box ι
π : Prepartition I
h : π.IsPartition
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = (splitMany I s).filter fun J => ↑J ⊆ ↑I
⊢ ∀ J ∈ splitMany I s, ↑J ⊆ ↑I

Proof state:
ι : Type u_1
inst✝ : Finite ι
I : Box ι
π : Prepartition I
h : π.IsPartition
⊢ ∃ s, splitMany I s ≤ π

Tactic:
refine (eventually_splitMany_inf_eq_filter π).exists.imp fun s hs => ?_

Result:
ι : Type u_1
inst✝ : Finite ι
I : Box ι
π : Prepartition I
h : π.IsPartition
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = (splitMany I s).filter fun J => ↑J ⊆ π.iUnion
⊢ splitMany I s ≤ π

Proof state:
case hp
ι : Type u_1
inst✝ : Finite ι
I : Box ι
π : Prepartition I
h : π.IsPartition
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = (splitMany I s).filter fun J => ↑J ⊆ ↑I
⊢ ∀ J ∈ splitMany I s, ↑J ⊆ ↑I

Tactic:
exact fun J hJ => le_of_mem _ hJ

Result:
no goals
-- Mathlib/Data/Nat/PSub.lean
theorem ppred_eq_some {m : ℕ} : ∀ {n}, ppred n = some m ↔ succ m = n
  | 0 => by constructor <;> intro h <;> contradiction
  | n + 1 => by constructor <;> intro h <;> injection h <;> subst m <;> rfl

Proof state:
m n : ℕ
⊢ (n + 1).ppred = some m ↔ m.succ = n + 1

Tactic:
constructor <;> intro h <;> injection h <;> subst m <;> rfl

Result:
no goals

Proof state:
m : ℕ
⊢ ppred 0 = some m ↔ m.succ = 0

Tactic:
constructor <;> intro h <;> contradiction

Result:
no goals
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
lemma fromCols_inj : Function.Injective2 (@fromCols R m n₁ n₂)

Proof state:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
⊢ Function.Injective2 fromCols

Tactic:
intros x1 x2 y1 y2

Result:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
x1 x2 : Matrix m n₁ R
y1 y2 : Matrix m n₂ R
⊢ x1.fromCols y1 = x2.fromCols y2 → x1 = x2 ∧ y1 = y2

Proof state:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
x1 x2 : Matrix m n₁ R
y1 y2 : Matrix m n₂ R
⊢ (∀ (i : m) (j : n₁ ⊕ n₂), x1.fromCols y1 i j = x2.fromCols y2 i j) →
    (∀ (i : m) (j : n₁), x1 i j = x2 i j) ∧ ∀ (i : m) (j : n₂), y1 i j = y2 i j

Tactic:
aesop

Result:
no goals

Proof state:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
x1 x2 : Matrix m n₁ R
y1 y2 : Matrix m n₂ R
⊢ x1.fromCols y1 = x2.fromCols y2 → x1 = x2 ∧ y1 = y2

Tactic:
simp only [funext_iff, ← Matrix.ext_iff]

Result:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
x1 x2 : Matrix m n₁ R
y1 y2 : Matrix m n₂ R
⊢ (∀ (i : m) (j : n₁ ⊕ n₂), x1.fromCols y1 i j = x2.fromCols y2 i j) →
    (∀ (i : m) (j : n₁), x1 i j = x2 i j) ∧ ∀ (i : m) (j : n₂), y1 i j = y2 i j
-- Mathlib/Algebra/Category/MonCat/Colimits.lean
theorem cocone_naturality_components (j j' : J) (f : j ⟶ j') (x : F.obj j) :
    (coconeMorphism F j') (F.map f x) = (coconeMorphism F j) x

Proof state:
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom (coconeMorphism F j')) ((ConcreteCategory.hom (F.map f)) x) =
    (ConcreteCategory.hom (coconeMorphism F j)) x

Tactic:
rw [← cocone_naturality F f]

Result:
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom (coconeMorphism F j')) ((ConcreteCategory.hom (F.map f)) x) =
    (ConcreteCategory.hom (F.map f ≫ coconeMorphism F j')) x

Proof state:
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom (coconeMorphism F j')) ((ConcreteCategory.hom (F.map f)) x) =
    (ConcreteCategory.hom (F.map f ≫ coconeMorphism F j')) x

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem lieSpan_le {K} : lieSpan R L s ≤ K ↔ s ⊆ K

Proof state:
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
K : LieSubalgebra R L
hs : s ⊆ ↑K
m : L
hm : m ∈ lieSpan R L s
⊢ m ∈ K

Tactic:
rw [mem_lieSpan] at hm

Result:
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
K : LieSubalgebra R L
hs : s ⊆ ↑K
m : L
hm : ∀ (K : LieSubalgebra R L), s ⊆ ↑K → m ∈ K
⊢ m ∈ K

Proof state:
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
K : LieSubalgebra R L
⊢ s ⊆ ↑K → lieSpan R L s ≤ K

Tactic:
intro hs m hm

Result:
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
K : LieSubalgebra R L
hs : s ⊆ ↑K
m : L
hm : m ∈ lieSpan R L s
⊢ m ∈ K

Proof state:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
K : LieSubalgebra R L
⊢ lieSpan R L s ≤ K → s ⊆ ↑K

Tactic:
exact Set.Subset.trans subset_lieSpan

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
K : LieSubalgebra R L
⊢ lieSpan R L s ≤ K ↔ s ⊆ ↑K

Tactic:
constructor

Result:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
K : LieSubalgebra R L
⊢ lieSpan R L s ≤ K → s ⊆ ↑K

case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
K : LieSubalgebra R L
⊢ s ⊆ ↑K → lieSpan R L s ≤ K

Proof state:
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
K : LieSubalgebra R L
hs : s ⊆ ↑K
m : L
hm : ∀ (K : LieSubalgebra R L), s ⊆ ↑K → m ∈ K
⊢ m ∈ K

Tactic:
exact hm _ hs

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean
theorem explicitCokernelDesc_comp_eq_zero {X Y Z W : SemiNormedGrp.{u}} {f : X ⟶ Y} {g : Y ⟶ Z}
    {h : Z ⟶ W} (cond : f ≫ g = 0) (cond2 : g ≫ h = 0) : explicitCokernelDesc cond ≫ h = 0

Proof state:
X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
cond2 : g ≫ h = 0
⊢ explicitCokernelDesc cond ≫ h = 0

Tactic:
rw [← cancel_epi (explicitCokernelπ f), ← Category.assoc, explicitCokernelπ_desc]

Result:
X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
cond2 : g ≫ h = 0
⊢ g ≫ h = explicitCokernelπ f ≫ 0

Proof state:
X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
cond2 : g ≫ h = 0
⊢ g ≫ h = explicitCokernelπ f ≫ 0

Tactic:
simp [cond2]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sqrtTwoAddSeries_two : sqrtTwoAddSeries 0 2 = √(2 + √2)

Proof state:
⊢ sqrtTwoAddSeries 0 2 = √(2 + √2)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Defs.lean
@[simp, norm_cast] lemma cast_pow {R : Type*} [Ring R] (n : ℤ) (m : ℕ) :
    ↑(n ^ m) = (n ^ m : R)

Proof state:
R : Type u_1
inst✝ : Ring R
n : ℤ
m : ℕ
⊢ ↑(n ^ m) = ↑n ^ m

Tactic:
induction' m with m ih <;> simp [_root_.pow_succ, *]

Result:
no goals