harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem map_extend_nhdsWithin_eq_image {y : M} (hy : y ∈ f.source) :
    map (f.extend I) (𝓝[s] y) = 𝓝[f.extend I '' ((f.extend I).source ∩ s)] f.extend I y

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
e : PartialEquiv M E := f.extend I
⊢ y ∈ (f.extend I).source

Tactic:
rwa [f.extend_source]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
⊢ map (↑(f.extend I)) (𝓝[s] y) = 𝓝[↑(f.extend I) '' ((f.extend I).source ∩ s)] ↑(f.extend I) y

Tactic:
set e := f.extend I

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
e : PartialEquiv M E := f.extend I
⊢ map (↑e) (𝓝[s] y) = 𝓝[↑e '' (e.source ∩ s)] ↑e y

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
e : PartialEquiv M E := f.extend I
⊢ map (↑e) (𝓝[s] y) = 𝓝[↑e '' (e.source ∩ s)] ↑e y

Tactic:
calc
  map e (𝓝[s] y) = map e (𝓝[e.source ∩ s] y) :=
    congr_arg (map e) (nhdsWithin_inter_of_mem (extend_source_mem_nhdsWithin f hy)).symm
  _ = 𝓝[e '' (e.source ∩ s)] e y :=
    ((f.extend I).leftInvOn.mono inter_subset_left).map_nhdsWithin_eq
      ((f.extend I).left_inv <| by rwa [f.extend_source])
      (continuousAt_extend_symm f hy).continuousWithinAt
      (continuousAt_extend f hy).continuousWithinAt

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem IsRotated.map {β : Type*} {l₁ l₂ : List α} (h : l₁ ~r l₂) (f : α → β) :
    map f l₁ ~r map f l₂

Proof state:
case intro
α : Type u
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
⊢ List.map f l₁ ~r List.map f (l₁.rotate n)

Tactic:
rw [map_rotate]

Result:
case intro
α : Type u
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
⊢ List.map f l₁ ~r (List.map f l₁).rotate n

Proof state:
case intro
α : Type u
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
⊢ List.map f l₁ ~r (List.map f l₁).rotate n

Tactic:
use n

Result:
no goals

Proof state:
α : Type u
β : Type u_1
l₁ l₂ : List α
h : l₁ ~r l₂
f : α → β
⊢ List.map f l₁ ~r List.map f l₂

Tactic:
obtain ⟨n, rfl⟩ := h

Result:
case intro
α : Type u
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
⊢ List.map f l₁ ~r List.map f (l₁.rotate n)
-- Mathlib/MeasureTheory/Group/MeasurableEquiv.lean
lemma dmaSMul_apply (μ : Measure A) (g : Gᵈᵐᵃ) (s : Set A) :
    (g • μ) s = μ (DomMulAct.mk.symm g • s)

Proof state:
case h.e_6.h
G : Type u_1
A : Type u_2
inst✝⁵ : Group G
inst✝⁴ : AddCommGroup A
inst✝³ : DistribMulAction G A
inst✝² : MeasurableSpace A
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G A
μ : Measure A
g : Gᵈᵐᵃ
s : Set A
⊢ ⇑(MeasurableEquiv.smul (DomMulAct.mk.symm g)⁻¹) ⁻¹' s = DomMulAct.mk.symm g • s

Tactic:
exact Set.preimage_smul_inv (DomMulAct.mk.symm g) s

Result:
no goals

Proof state:
G : Type u_1
A : Type u_2
inst✝⁵ : Group G
inst✝⁴ : AddCommGroup A
inst✝³ : DistribMulAction G A
inst✝² : MeasurableSpace A
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G A
μ : Measure A
g : Gᵈᵐᵃ
s : Set A
⊢ μ (⇑(MeasurableEquiv.smul (DomMulAct.mk.symm g)⁻¹) ⁻¹' s) = μ (DomMulAct.mk.symm g • s)

Tactic:
congr 1

Result:
case h.e_6.h
G : Type u_1
A : Type u_2
inst✝⁵ : Group G
inst✝⁴ : AddCommGroup A
inst✝³ : DistribMulAction G A
inst✝² : MeasurableSpace A
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G A
μ : Measure A
g : Gᵈᵐᵃ
s : Set A
⊢ ⇑(MeasurableEquiv.smul (DomMulAct.mk.symm g)⁻¹) ⁻¹' s = DomMulAct.mk.symm g • s

Proof state:
G : Type u_1
A : Type u_2
inst✝⁵ : Group G
inst✝⁴ : AddCommGroup A
inst✝³ : DistribMulAction G A
inst✝² : MeasurableSpace A
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G A
μ : Measure A
g : Gᵈᵐᵃ
s : Set A
⊢ (g • μ) s = μ (DomMulAct.mk.symm g • s)

Tactic:
refine ((MeasurableEquiv.smul ((DomMulAct.mk.symm g : G)⁻¹)).map_apply _).trans ?_

Result:
G : Type u_1
A : Type u_2
inst✝⁵ : Group G
inst✝⁴ : AddCommGroup A
inst✝³ : DistribMulAction G A
inst✝² : MeasurableSpace A
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G A
μ : Measure A
g : Gᵈᵐᵃ
s : Set A
⊢ μ (⇑(MeasurableEquiv.smul (DomMulAct.mk.symm g)⁻¹) ⁻¹' s) = μ (DomMulAct.mk.symm g • s)
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem iterate_pos_eq_iff {x : ℝ} {m : ℤ} {n : ℕ} (hn : 0 < n) :
    f^[n] x = x + n * m ↔ f x = x + m

Proof state:
f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (⇑f)^[n] x = x + ↑n * ↑m ↔ f x = x + ↑m

Tactic:
simpa only [nsmul_eq_mul, add_right_iterate] using
  (f.commute_add_int m).iterate_pos_eq_iff_map_eq f.monotone (strictMono_id.add_const (m : ℝ)) hn

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem Coprime.mul_add_mul_ne_mul {m n a b : ℕ} (cop : Coprime m n) (ha : a ≠ 0) (hb : b ≠ 0) :
    a * m + b * n ≠ m * n

Proof state:
m n a b : ℕ
cop : m.Coprime n
ha : a ≠ 0
hb : b ≠ 0
h : a * m + b * n = m * n
⊢ False

Tactic:
obtain ⟨x, rfl⟩ : n ∣ a :=
  cop.symm.dvd_of_dvd_mul_right
    ((Nat.dvd_add_iff_left (Nat.dvd_mul_left n b)).mpr
      ((congr_arg _ h).mpr (Nat.dvd_mul_left n m)))

Result:
case intro
m n b : ℕ
cop : m.Coprime n
hb : b ≠ 0
x : ℕ
ha : n * x ≠ 0
h : n * x * m + b * n = m * n
⊢ False

Proof state:
case intro.intro
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ (x + y) * (m * n) = m * n

Tactic:
rw [← mul_assoc, ← h, Nat.add_mul, Nat.add_mul, mul_comm _ n, ← mul_assoc, mul_comm y]

Result:
no goals

Proof state:
case intro
m n b : ℕ
cop : m.Coprime n
hb : b ≠ 0
x : ℕ
ha : n * x ≠ 0
h : n * x * m + b * n = m * n
⊢ False

Tactic:
obtain ⟨y, rfl⟩ : m ∣ b :=
  cop.dvd_of_dvd_mul_right
    ((Nat.dvd_add_iff_right (Nat.dvd_mul_left m (n * x))).mpr
      ((congr_arg _ h).mpr (Nat.dvd_mul_right m n)))

Result:
case intro.intro
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : n * x ≠ 0
y : ℕ
hb : m * y ≠ 0
h : n * x * m + m * y * n = m * n
⊢ False

Proof state:
m n a b : ℕ
cop : m.Coprime n
ha : a ≠ 0
hb : b ≠ 0
⊢ a * m + b * n ≠ m * n

Tactic:
intro h

Result:
m n a b : ℕ
cop : m.Coprime n
ha : a ≠ 0
hb : b ≠ 0
h : a * m + b * n = m * n
⊢ False

Proof state:
case intro.intro
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : n * x ≠ 0
y : ℕ
hb : m * y ≠ 0
h : n * x * m + m * y * n = m * n
⊢ False

Tactic:
rw [mul_comm, mul_ne_zero_iff, ← one_le_iff_ne_zero] at ha hb

Result:
case intro.intro
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ False

Proof state:
case intro.intro
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ False

Tactic:
refine mul_ne_zero hb.2 ha.2 (eq_zero_of_mul_eq_self_left (ne_of_gt (add_le_add ha.1 hb.1)) ?_)

Result:
case intro.intro
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ (x + y) * (m * n) = m * n
-- Mathlib/Order/PiLex.lean
theorem Lex.noMaxOrder' [Preorder ι] [∀ i, LT (β i)] (i : ι) [NoMaxOrder (β i)] :
    NoMaxOrder (Lex (∀ i, β i)) :=
  ⟨fun a => by
    let ⟨b, hb⟩ := exists_gt (a i)
    classical
    exact ⟨Function.update a i b, i, fun j hj =>
      (Function.update_of_ne hj.ne b a).symm, by rwa [Function.update_self i b]⟩⟩

Proof state:
ι : Type u_1
β : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
i : ι
inst✝ : NoMaxOrder (β i)
a : Lex ((i : ι) → β i)
b : β i
hb : a i < b
⊢ ∃ b, a < b

Tactic:
exact ⟨Function.update a i b, i, fun j hj =>
  (Function.update_of_ne hj.ne b a).symm, by rwa [Function.update_self i b]⟩

Result:
no goals

Proof state:
ι : Type u_1
β : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
i : ι
inst✝ : NoMaxOrder (β i)
a : Lex ((i : ι) → β i)
⊢ ∃ b, a < b

Tactic:
let ⟨b, hb⟩ := exists_gt (a i)

Result:
ι : Type u_1
β : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
i : ι
inst✝ : NoMaxOrder (β i)
a : Lex ((i : ι) → β i)
b : β i
hb : a i < b
⊢ ∃ b, a < b

Proof state:
ι : Type u_1
β : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
i : ι
inst✝ : NoMaxOrder (β i)
a : Lex ((i : ι) → β i)
b : β i
hb : a i < b
⊢ (fun x x1 x2 => x1 < x2) i (a i) (Function.update a i b i)

Tactic:
rwa [Function.update_self i b]

Result:
no goals

Proof state:
ι : Type u_1
β : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
i : ι
inst✝ : NoMaxOrder (β i)
a : Lex ((i : ι) → β i)
b : β i
hb : a i < b
⊢ ∃ b, a < b

Tactic:
classical
exact ⟨Function.update a i b, i, fun j hj =>
  (Function.update_of_ne hj.ne b a).symm, by rwa [Function.update_self i b]⟩

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
lemma mgf_dirac {x : ℝ} (hX : μ.map X = .dirac x) (t : ℝ) : mgf X μ t = exp (x * t)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Measure.map X μ = Measure.dirac x
t : ℝ
⊢ IsProbabilityMeasure (Measure.map X μ)

Tactic:
rw [hX]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Measure.map X μ = Measure.dirac x
t : ℝ
⊢ IsProbabilityMeasure (Measure.dirac x)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Measure.map X μ = Measure.dirac x
t : ℝ
⊢ IsProbabilityMeasure (Measure.dirac x)

Tactic:
infer_instance

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Measure.map X μ = Measure.dirac x
t : ℝ
⊢ mgf X μ t = rexp (x * t)

Tactic:
have : IsProbabilityMeasure (μ.map X) := by rw [hX]; infer_instance

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Measure.map X μ = Measure.dirac x
t : ℝ
this : IsProbabilityMeasure (Measure.map X μ)
⊢ mgf X μ t = rexp (x * t)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Measure.map X μ = Measure.dirac x
t : ℝ
this : IsProbabilityMeasure (Measure.map X μ)
⊢ mgf X μ t = rexp (x * t)

Tactic:
rw [← mgf_id_map (.of_map_ne_zero <| IsProbabilityMeasure.ne_zero _), mgf, hX, integral_dirac,
  mul_comm, id_def]

Result:
no goals
-- Mathlib/Topology/Compactness/Lindelof.lean
lemma eq_open_union_countable [HereditarilyLindelofSpace X] {ι : Type u} (U : ι → Set X)
    (h : ∀ i, IsOpen (U i)) : ∃ t : Set ι, t.Countable ∧ ⋃ i∈t, U i = ⋃ i, U i

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u
U : ι → Set X
h : ∀ (i : ι), IsOpen (U i)
⊢ ∃ t, t.Countable ∧ ⋃ i ∈ t, U i = ⋃ i, U i

Tactic:
have : IsLindelof (⋃ i, U i) := HereditarilyLindelof_LindelofSets (⋃ i, U i)

Result:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u
U : ι → Set X
h : ∀ (i : ι), IsOpen (U i)
this : IsLindelof (⋃ i, U i)
⊢ ∃ t, t.Countable ∧ ⋃ i ∈ t, U i = ⋃ i, U i

Proof state:
case intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u
U : ι → Set X
h : ∀ (i : ι), IsOpen (U i)
this : IsLindelof (⋃ i, U i)
t : Set ι
htc : t.Countable
htu : ⋃ i, U i ⊆ ⋃ i ∈ t, U i
⊢ ∃ t, t.Countable ∧ ⋃ i ∈ t, U i = ⋃ i, U i

Tactic:
use t, htc

Result:
case right
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u
U : ι → Set X
h : ∀ (i : ι), IsOpen (U i)
this : IsLindelof (⋃ i, U i)
t : Set ι
htc : t.Countable
htu : ⋃ i, U i ⊆ ⋃ i ∈ t, U i
⊢ ⋃ i ∈ t, U i = ⋃ i, U i

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u
U : ι → Set X
h : ∀ (i : ι), IsOpen (U i)
this : IsLindelof (⋃ i, U i)
⊢ ∃ t, t.Countable ∧ ⋃ i ∈ t, U i = ⋃ i, U i

Tactic:
rcases isLindelof_iff_countable_subcover.mp this U h (Eq.subset rfl) with ⟨t, ⟨htc, htu⟩⟩

Result:
case intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u
U : ι → Set X
h : ∀ (i : ι), IsOpen (U i)
this : IsLindelof (⋃ i, U i)
t : Set ι
htc : t.Countable
htu : ⋃ i, U i ⊆ ⋃ i ∈ t, U i
⊢ ∃ t, t.Countable ∧ ⋃ i ∈ t, U i = ⋃ i, U i

Proof state:
case right
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u
U : ι → Set X
h : ∀ (i : ι), IsOpen (U i)
this : IsLindelof (⋃ i, U i)
t : Set ι
htc : t.Countable
htu : ⋃ i, U i ⊆ ⋃ i ∈ t, U i
⊢ ⋃ i ∈ t, U i = ⋃ i, U i

Tactic:
apply eq_of_subset_of_subset (iUnion₂_subset_iUnion (fun i ↦ i ∈ t) fun i ↦ U i) htu

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem add_le_add_iff_of_lt_aleph0 {α β γ : Cardinal} (γ₀ : γ < ℵ₀) :
    α + γ ≤ β + γ ↔ α ≤ β

Proof state:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : α + γ ≤ β + γ
⊢ α ≤ β

Tactic:
contrapose h

Result:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : ¬α ≤ β
⊢ ¬α + γ ≤ β + γ

Proof state:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
⊢ α + γ ≤ β + γ ↔ α ≤ β

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

Result:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : α + γ ≤ β + γ
⊢ α ≤ β

Proof state:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : ¬α ≤ β
⊢ ¬α + γ ≤ β + γ

Tactic:
rw [not_le, lt_iff_le_and_ne, Ne] at h ⊢

Result:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : β ≤ α ∧ ¬β = α
⊢ β + γ ≤ α + γ ∧ ¬β + γ = α + γ

Proof state:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : β ≤ α ∧ ¬β = α
⊢ β + γ ≤ α + γ ∧ ¬β + γ = α + γ

Tactic:
exact ⟨add_le_add_right h.1 γ, mt (add_right_inj_of_lt_aleph0 γ₀).1 h.2⟩

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem ofMul_image_powers_eq_multiples_ofMul [Monoid M] {x : M} :
    Additive.ofMul '' (Submonoid.powers x : Set M) = AddSubmonoid.multiples (Additive.ofMul x)

Proof state:
case h.mp.intro.intro.intro
M : Type u_1
inst✝ : Monoid M
x : M
x✝ : Additive M
y : M
hy2 : Additive.ofMul y = x✝
n : ℕ
hy1 : (fun x_1 => x ^ x_1) n = y
⊢ x✝ ∈ ↑(AddSubmonoid.multiples (Additive.ofMul x))

Tactic:
use n

Result:
case h
M : Type u_1
inst✝ : Monoid M
x : M
x✝ : Additive M
y : M
hy2 : Additive.ofMul y = x✝
n : ℕ
hy1 : (fun x_1 => x ^ x_1) n = y
⊢ (fun i => i • Additive.ofMul x) n = x✝

Proof state:
M : Type u_1
inst✝ : Monoid M
x : M
⊢ ⇑Additive.ofMul '' ↑(Submonoid.powers x) = ↑(AddSubmonoid.multiples (Additive.ofMul x))

Tactic:
ext

Result:
case h
M : Type u_1
inst✝ : Monoid M
x : M
x✝ : Additive M
⊢ x✝ ∈ ⇑Additive.ofMul '' ↑(Submonoid.powers x) ↔ x✝ ∈ ↑(AddSubmonoid.multiples (Additive.ofMul x))

Proof state:
case h.mp
M : Type u_1
inst✝ : Monoid M
x : M
x✝ : Additive M
⊢ x✝ ∈ ⇑Additive.ofMul '' ↑(Submonoid.powers x) → x✝ ∈ ↑(AddSubmonoid.multiples (Additive.ofMul x))

Tactic:
rintro ⟨y, ⟨n, hy1⟩, hy2⟩

Result:
case h.mp.intro.intro.intro
M : Type u_1
inst✝ : Monoid M
x : M
x✝ : Additive M
y : M
hy2 : Additive.ofMul y = x✝
n : ℕ
hy1 : (fun x_1 => x ^ x_1) n = y
⊢ x✝ ∈ ↑(AddSubmonoid.multiples (Additive.ofMul x))

Proof state:
case h.mpr.intro
M : Type u_1
inst✝ : Monoid M
x : M
x✝ : Additive M
n : ℕ
hn : (fun i => i • Additive.ofMul x) n = x✝
⊢ Additive.ofMul (x ^ n) = x✝

Tactic:
rwa [ofMul_pow]

Result:
no goals

Proof state:
case h
M : Type u_1
inst✝ : Monoid M
x : M
x✝ : Additive M
⊢ x✝ ∈ ⇑Additive.ofMul '' ↑(Submonoid.powers x) ↔ x✝ ∈ ↑(AddSubmonoid.multiples (Additive.ofMul x))

Tactic:
constructor

Result:
case h.mp
M : Type u_1
inst✝ : Monoid M
x : M
x✝ : Additive M
⊢ x✝ ∈ ⇑Additive.ofMul '' ↑(Submonoid.powers x) → x✝ ∈ ↑(AddSubmonoid.multiples (Additive.ofMul x))

case h.mpr
M : Type u_1
inst✝ : Monoid M
x : M
x✝ : Additive M
⊢ x✝ ∈ ↑(AddSubmonoid.multiples (Additive.ofMul x)) → x✝ ∈ ⇑Additive.ofMul '' ↑(Submonoid.powers x)

Proof state:
case h.mpr
M : Type u_1
inst✝ : Monoid M
x : M
x✝ : Additive M
⊢ x✝ ∈ ↑(AddSubmonoid.multiples (Additive.ofMul x)) → x✝ ∈ ⇑Additive.ofMul '' ↑(Submonoid.powers x)

Tactic:
rintro ⟨n, hn⟩

Result:
case h.mpr.intro
M : Type u_1
inst✝ : Monoid M
x : M
x✝ : Additive M
n : ℕ
hn : (fun i => i • Additive.ofMul x) n = x✝
⊢ x✝ ∈ ⇑Additive.ofMul '' ↑(Submonoid.powers x)

Proof state:
case h
M : Type u_1
inst✝ : Monoid M
x : M
x✝ : Additive M
y : M
hy2 : Additive.ofMul y = x✝
n : ℕ
hy1 : (fun x_1 => x ^ x_1) n = y
⊢ (fun i => i • Additive.ofMul x) n = x✝

Tactic:
simpa [← ofMul_pow, hy1]

Result:
no goals

Proof state:
case h.mpr.intro
M : Type u_1
inst✝ : Monoid M
x : M
x✝ : Additive M
n : ℕ
hn : (fun i => i • Additive.ofMul x) n = x✝
⊢ x✝ ∈ ⇑Additive.ofMul '' ↑(Submonoid.powers x)

Tactic:
refine ⟨x ^ n, ⟨n, rfl⟩, ?_⟩

Result:
case h.mpr.intro
M : Type u_1
inst✝ : Monoid M
x : M
x✝ : Additive M
n : ℕ
hn : (fun i => i • Additive.ofMul x) n = x✝
⊢ Additive.ofMul (x ^ n) = x✝
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_X_pow (n : ℕ) : derivative (X ^ n : R[X]) = C (n : R) * X ^ (n - 1)

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ derivative (X ^ n) = C ↑n * X ^ (n - 1)

Tactic:
convert derivative_C_mul_X_pow (1 : R) n <;> simp

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma not_isUnramified_iff_card_stabilizer_eq_two [IsGalois k K] :
    ¬ IsUnramified k w ↔ Nat.card (Stab w) = 2

Proof state:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
⊢ ¬Nat.card ↥(Stab w) = 1 ↔ Nat.card ↥(Stab w) = 2

Tactic:
obtain (e|e) := nat_card_stabilizer_eq_one_or_two k w <;> rw [e] <;> decide

Result:
no goals

Proof state:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
⊢ ¬IsUnramified k w ↔ Nat.card ↥(Stab w) = 2

Tactic:
rw [isUnramified_iff_card_stabilizer_eq_one]

Result:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
⊢ ¬Nat.card ↥(Stab w) = 1 ↔ Nat.card ↥(Stab w) = 2
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean
theorem find?_succ {p : Fin (n+1) → Bool} :
    find? p = if p 0 then some 0 else (find? fun i => p i.succ).map Fin.succ

Proof state:
n : Nat
p : Fin (n + 1) → Bool
⊢ ((if p 0 = true then some 0 else none) <|> findSome? fun i => if p i.succ = true then some i.succ else none) =
    if p 0 = true then some 0 else Option.map succ (findSome? (Option.guard fun a => p a.succ = true))

Tactic:
split <;> simp [Option.none_orElse, map_findSome?, Function.comp_def, Option.guard]

Result:
no goals

Proof state:
n : Nat
p : Fin (n + 1) → Bool
⊢ find? p = if p 0 = true then some 0 else Option.map succ (find? fun i => p i.succ)

Tactic:
simp only [find?, findSome?_succ, Option.guard]

Result:
n : Nat
p : Fin (n + 1) → Bool
⊢ ((if p 0 = true then some 0 else none) <|> findSome? fun i => if p i.succ = true then some i.succ else none) =
    if p 0 = true then some 0 else Option.map succ (findSome? (Option.guard fun a => p a.succ = true))
-- Mathlib/RingTheory/Nilpotent/Basic.lean
theorem isNilpotent_add (h_comm : Commute x y) (hx : IsNilpotent x) (hy : IsNilpotent y) :
    IsNilpotent (x + y)

Proof state:
case intro.intro
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
⊢ IsNilpotent (x + y)

Tactic:
exact ⟨_, add_pow_add_eq_zero_of_pow_eq_zero h_comm hn hm⟩

Result:
no goals

Proof state:
case intro
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : IsNilpotent y
n : ℕ
hn : x ^ n = 0
⊢ IsNilpotent (x + y)

Tactic:
obtain ⟨m, hm⟩ := hy

Result:
case intro.intro
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
⊢ IsNilpotent (x + y)

Proof state:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : IsNilpotent x
hy : IsNilpotent y
⊢ IsNilpotent (x + y)

Tactic:
obtain ⟨n, hn⟩ := hx

Result:
case intro
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : IsNilpotent y
n : ℕ
hn : x ^ n = 0
⊢ IsNilpotent (x + y)
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem degree_eq_card_roots {p : K[X]} {i : K →+* L} (p_ne_zero : p ≠ 0) (hsplit : Splits i p) :
    p.degree = Multiset.card (p.map i).roots

Proof state:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
p : K[X]
i : K →+* L
p_ne_zero : p ≠ 0
hsplit : Splits i p
⊢ p.degree = ↑(map i p).roots.card

Tactic:
rw [degree_eq_natDegree p_ne_zero, natDegree_eq_card_roots hsplit]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem getElem_range' (start size step i) (h : i < size) :
   (range' start size step)[i] = start + step * i

Proof state:
start size step i : Nat
h : i < size
⊢ (range' start size step)[i] = start + step * i

Tactic:
simp [range', h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_size_eq_size {p : α → Bool} {l : Array α} :
    (filter p l).size = l.size ↔ ∀ a ∈ l, p a

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ (filter p l).size = l.size ↔ ∀ (a : α), a ∈ l → p a = true

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p : α → Bool
l : List α
⊢ (filter p { toList := l }).size = { toList := l }.size ↔ ∀ (a : α), a ∈ { toList := l } → p a = true

Proof state:
case mk
α : Type u_1
p : α → Bool
l : List α
⊢ (filter p { toList := l }).size = { toList := l }.size ↔ ∀ (a : α), a ∈ { toList := l } → p a = true

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Disjointed.lean
theorem disjointed_unique {f d : ι → α} (hdisj : ∀ {i j : ι} (_ : i < j), Disjoint (d i) (d j))
    (hsups : partialSups d = partialSups f) :
    d = disjointed f

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f d : ι → α
hdisj : ∀ {i j : ι}, i < j → Disjoint (d i) (d j)
hsups : partialSups d = partialSups f
⊢ d = disjointed f

Tactic:
rw [← disjointed_partialSups, ← hsups, disjointed_partialSups]

Result:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f d : ι → α
hdisj : ∀ {i j : ι}, i < j → Disjoint (d i) (d j)
hsups : partialSups d = partialSups f
⊢ d = disjointed d

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f d : ι → α
hdisj : ∀ {i j : ι}, i < j → Disjoint (d i) (d j)
hsups : partialSups d = partialSups f
⊢ d = disjointed d

Tactic:
exact funext fun _ ↦ (disjointed_eq_self (fun _ hj ↦ hdisj hj)).symm

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem monic_of_c_eq_one (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 1) : P.toPoly.Monic

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 1
⊢ P.toPoly.Monic

Tactic:
nontriviality R

Result:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 1
a✝ : Nontrivial R
⊢ P.toPoly.Monic

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 1
a✝ : Nontrivial R
⊢ P.toPoly.Monic

Tactic:
rw [Monic, leadingCoeff_of_c_ne_zero ha hb (hc ▸ one_ne_zero), hc]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem eq_inv_mul_iff_mul_eq {a c : α} : a = ↑b⁻¹ * c ↔ ↑b * a = c :=
  ⟨fun h => by rw [h, mul_inv_cancel_left], fun h => by rw [← h, inv_mul_cancel_left]⟩

Proof state:
α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : ↑b * a = c
⊢ a = ↑b⁻¹ * c

Tactic:
rw [← h, inv_mul_cancel_left]

Result:
no goals

Proof state:
α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : a = ↑b⁻¹ * c
⊢ ↑b * a = c

Tactic:
rw [h, mul_inv_cancel_left]

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
theorem inv_mul_cancel_right (a b : G) : a * b⁻¹ * b = a

Proof state:
G : Type u_1
inst✝ : Group G
a b : G
⊢ a * b⁻¹ * b = a

Tactic:
rw [mul_assoc, inv_mul_cancel, mul_one]

Result:
no goals