harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/LocalRing/RingHom/Basic.lean
theorem RingHom.domain_isLocalRing {R S : Type*} [CommSemiring R] [CommSemiring S] [IsLocalRing S]
    (f : R →+* S) [IsLocalHom f] : IsLocalRing R

Proof state:
case h
R : Type u_4
S : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : IsLocalRing S
f : R →+* S
inst✝ : IsLocalHom f
this : Nontrivial R
a b : R
⊢ f a ∈ nonunits S → f b ∈ nonunits S → f a + f b ∈ nonunits S

Tactic:
exact IsLocalRing.nonunits_add

Result:
no goals

Proof state:
R : Type u_4
S : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : IsLocalRing S
f : R →+* S
inst✝ : IsLocalHom f
⊢ IsLocalRing R

Tactic:
haveI : Nontrivial R := f.domain_nontrivial

Result:
R : Type u_4
S : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : IsLocalRing S
f : R →+* S
inst✝ : IsLocalHom f
this : Nontrivial R
⊢ IsLocalRing R

Proof state:
R : Type u_4
S : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : IsLocalRing S
f : R →+* S
inst✝ : IsLocalHom f
this : Nontrivial R
⊢ IsLocalRing R

Tactic:
apply IsLocalRing.of_nonunits_add

Result:
case h
R : Type u_4
S : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : IsLocalRing S
f : R →+* S
inst✝ : IsLocalHom f
this : Nontrivial R
⊢ ∀ (a b : R), a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R

Proof state:
case h
R : Type u_4
S : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : IsLocalRing S
f : R →+* S
inst✝ : IsLocalHom f
this : Nontrivial R
⊢ ∀ (a b : R), a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R

Tactic:
intro a b

Result:
case h
R : Type u_4
S : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : IsLocalRing S
f : R →+* S
inst✝ : IsLocalHom f
this : Nontrivial R
a b : R
⊢ a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R

Proof state:
case h
R : Type u_4
S : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : IsLocalRing S
f : R →+* S
inst✝ : IsLocalHom f
this : Nontrivial R
a b : R
⊢ a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R

Tactic:
simp_rw [← map_mem_nonunits_iff f, f.map_add]

Result:
case h
R : Type u_4
S : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : IsLocalRing S
f : R →+* S
inst✝ : IsLocalHom f
this : Nontrivial R
a b : R
⊢ f a ∈ nonunits S → f b ∈ nonunits S → f a + f b ∈ nonunits S
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem LinearIsometryEquiv.norm_iteratedFDeriv_comp_left (g : F ≃ₗᵢ[𝕜] G) (f : E → F) (x : E)
    (i : ℕ) : ‖iteratedFDeriv 𝕜 i (g ∘ f) x‖ = ‖iteratedFDeriv 𝕜 i f 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
g : F ≃ₗᵢ[𝕜] G
f : E → F
x : E
i : ℕ
⊢ ‖iteratedFDeriv 𝕜 i (⇑g ∘ f) x‖ = ‖iteratedFDeriv 𝕜 i f x‖

Tactic:
rw [← iteratedFDerivWithin_univ, ← 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
g : F ≃ₗᵢ[𝕜] G
f : E → F
x : E
i : ℕ
⊢ ‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) univ x‖ = ‖iteratedFDerivWithin 𝕜 i f 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
g : F ≃ₗᵢ[𝕜] G
f : E → F
x : E
i : ℕ
⊢ ‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) univ x‖ = ‖iteratedFDerivWithin 𝕜 i f univ x‖

Tactic:
apply g.norm_iteratedFDerivWithin_comp_left f uniqueDiffOn_univ (mem_univ x) i

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem Indep.indep_isRestriction (hI : M.Indep I) (hNM : N ≤r M) (hIN : I ⊆ N.E) : N.Indep I

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
R : Set α
hIN : I ⊆ (M ↾ R).E
⊢ (M ↾ R).Indep I

Tactic:
simpa [hI]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I : Set α
N : Matroid α
hI : M.Indep I
hNM : N ≤r M
hIN : I ⊆ N.E
⊢ N.Indep I

Tactic:
obtain ⟨R, -, rfl⟩ := hNM

Result:
case intro.intro
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
R : Set α
hIN : I ⊆ (M ↾ R).E
⊢ (M ↾ R).Indep I
-- Mathlib/MeasureTheory/Group/Convolution.lean
theorem mconv_dirac_one [MeasurableMul₂ M]
    (μ : Measure M) [SFinite μ] : μ ∗ (Measure.dirac 1) = μ

Proof state:
M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
⊢ Measurable fun x => x.1 * x.2

Tactic:
fun_prop

Result:
no goals

Proof state:
M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
⊢ map (fun x => x.1 * x.2) (μ.prod (dirac 1)) = μ

Tactic:
rw [MeasureTheory.Measure.prod_dirac, map_map (by fun_prop)]

Result:
M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
⊢ map ((fun x => x.1 * x.2) ∘ fun x => (x, 1)) μ = μ

M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
⊢ Measurable fun x => (x, 1)

Proof state:
M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
⊢ map ((fun x => x.1 * x.2) ∘ fun x => (x, 1)) μ = μ

Tactic:
simp only [Function.comp_def, mul_one, map_id']

Result:
no goals

Proof state:
M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
⊢ Measurable fun x => (x, 1)

Tactic:
fun_prop

Result:
no goals

Proof state:
M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
⊢ μ ∗ dirac 1 = μ

Tactic:
unfold mconv

Result:
M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
⊢ map (fun x => x.1 * x.2) (μ.prod (dirac 1)) = μ
-- Mathlib/Topology/Connected/TotallyDisconnected.lean
theorem isTotallyDisconnected_of_isTotallySeparated {s : Set α} (H : IsTotallySeparated s) :
    IsTotallyDisconnected s

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
⊢ IsTotallyDisconnected s

Tactic:
intro t hts ht x x_in y y_in

Result:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
⊢ x = y

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
⊢ False

Tactic:
obtain
  ⟨u : Set α, v : Set α, hu : IsOpen u, hv : IsOpen v, hxu : x ∈ u, hyv : y ∈ v, hs : s ⊆ u ∪ v,
    huv⟩ :=
  H (hts x_in) (hts y_in) h

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
u v : Set α
hu : IsOpen u
hv : IsOpen v
hxu : x ∈ u
hyv : y ∈ v
hs : s ⊆ u ∪ v
huv : Disjoint u v
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
u v : Set α
hu : IsOpen u
hv : IsOpen v
hxu : x ∈ u
hyv : y ∈ v
hs : s ⊆ u ∪ v
huv : Disjoint u v
⊢ t ∩ (u ∩ v) = ∅

Tactic:
rw [huv.inter_eq, inter_empty]

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
⊢ x = y

Tactic:
by_contra h

Result:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
u v : Set α
hu : IsOpen u
hv : IsOpen v
hxu : x ∈ u
hyv : y ∈ v
hs : s ⊆ u ∪ v
huv : Disjoint u v
⊢ False

Tactic:
refine (ht _ _ hu hv (hts.trans hs) ⟨x, x_in, hxu⟩ ⟨y, y_in, hyv⟩).ne_empty ?_

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
u v : Set α
hu : IsOpen u
hv : IsOpen v
hxu : x ∈ u
hyv : y ∈ v
hs : s ⊆ u ∪ v
huv : Disjoint u v
⊢ t ∩ (u ∩ v) = ∅
-- Mathlib/Analysis/MeanInequalitiesPow.lean
theorem rpow_add_rpow_le {p q : ℝ} (a b : ℝ≥0∞) (hp_pos : 0 < p) (hpq : p ≤ q) :
    (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)

Proof state:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)

Tactic:
have h_rpow_add_rpow_le_add :
  ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p := by
  refine rpow_add_rpow_le_add (a ^ p) (b ^ p) ?_
  rwa [one_le_div hp_pos]

Result:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)

Proof state:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
⊢ 1 ≤ q / p

Tactic:
rwa [one_le_div hp_pos]

Result:
no goals

Proof state:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)

Tactic:
rw [h_rpow a, h_rpow b, one_div p, ENNReal.le_rpow_inv_iff hp_pos, ← ENNReal.rpow_mul, mul_comm,
  mul_one_div]

Result:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p

Proof state:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p

Tactic:
rwa [one_div_div] at h_rpow_add_rpow_le_add

Result:
no goals

Proof state:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p

Tactic:
refine rpow_add_rpow_le_add (a ^ p) (b ^ p) ?_

Result:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
⊢ 1 ≤ q / p

Proof state:
p q : ℝ
a✝ b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0∞
⊢ a ^ q = (a ^ p) ^ (q / p)

Tactic:
rw [← ENNReal.rpow_mul, mul_div_cancel₀ _ hp_pos.ne']

Result:
no goals

Proof state:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)

Tactic:
have h_rpow : ∀ a : ℝ≥0∞, a ^ q = (a ^ p) ^ (q / p) := fun a => by
  rw [← ENNReal.rpow_mul, mul_div_cancel₀ _ hp_pos.ne']

Result:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Certificate.of_combine (ctx : Context) (cs : Certificate) (h : cs.combine.denote ctx → False) : cs.denote ctx

Proof state:
ctx : Context
cs✝ : Certificate
k : Nat
c : ExprCnstr
cs : List (Nat × ExprCnstr)
h : ¬PolyCnstr.denote ctx (combineHyps (PolyCnstr.mul (k + 1) c.toNormPoly) cs)
⊢ ExprCnstr.denote ctx c → denote ctx cs

Tactic:
intro h'

Result:
ctx : Context
cs✝ : Certificate
k : Nat
c : ExprCnstr
cs : List (Nat × ExprCnstr)
h : ¬PolyCnstr.denote ctx (combineHyps (PolyCnstr.mul (k + 1) c.toNormPoly) cs)
h' : ExprCnstr.denote ctx c
⊢ denote ctx cs

Proof state:
ctx : Context
cs : Certificate
h : PolyCnstr.denote ctx (combine []) → False
⊢ denote ctx []

Tactic:
simp [combine, PolyCnstr.denote, Poly.denote_eq] at h

Result:
no goals

Proof state:
ctx : Context
cs✝ : Certificate
k : Nat
c : ExprCnstr
cs : List (Nat × ExprCnstr)
h : ¬PolyCnstr.denote ctx (combineHyps (PolyCnstr.mul (k + 1) c.toNormPoly) cs)
h' : ExprCnstr.denote ctx c
⊢ denote ctx cs

Tactic:
apply of_combineHyps (h := h)

Result:
ctx : Context
cs✝ : Certificate
k : Nat
c : ExprCnstr
cs : List (Nat × ExprCnstr)
h : ¬PolyCnstr.denote ctx (combineHyps (PolyCnstr.mul (k + 1) c.toNormPoly) cs)
h' : ExprCnstr.denote ctx c
⊢ PolyCnstr.denote ctx (PolyCnstr.mul (k + 1) c.toNormPoly)

Proof state:
ctx : Context
cs✝ : Certificate
k : Nat
c : ExprCnstr
cs : List (Nat × ExprCnstr)
h : ¬PolyCnstr.denote ctx (combineHyps (PolyCnstr.mul (k + 1) c.toNormPoly) cs)
h' : ExprCnstr.denote ctx c
⊢ PolyCnstr.denote ctx (PolyCnstr.mul (k + 1) c.toNormPoly)

Tactic:
simp [h']

Result:
no goals

Proof state:
ctx : Context
cs✝ : Certificate
k : Nat
c : ExprCnstr
cs : List (Nat × ExprCnstr)
h : PolyCnstr.denote ctx (combine ((k, c) :: cs)) → False
⊢ denote ctx ((k, c) :: cs)

Tactic:
simp [denote, combine] at *

Result:
ctx : Context
cs✝ : Certificate
k : Nat
c : ExprCnstr
cs : List (Nat × ExprCnstr)
h : ¬PolyCnstr.denote ctx (combineHyps (PolyCnstr.mul (k + 1) c.toNormPoly) cs)
⊢ ExprCnstr.denote ctx c → denote ctx cs

Proof state:
ctx : Context
cs : Certificate
h : PolyCnstr.denote ctx cs.combine → False
⊢ denote ctx cs

Tactic:
match cs with
| [] => simp [combine, PolyCnstr.denote, Poly.denote_eq] at h
| (k, c)::cs =>
  simp [denote, combine] at *
  intro h'
  apply of_combineHyps (h := h)
  simp [h']

Result:
no goals
-- Mathlib/Data/Nat/Cast/Commute.lean
theorem cast_commute (n : ℕ) (x : α) : Commute (n : α) x

Proof state:
case zero
α : Type u_1
inst✝ : NonAssocSemiring α
x : α
⊢ Commute 0 x

Tactic:
exact Commute.zero_left x

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n) x
⊢ Commute (↑(n + 1)) x

Tactic:
rw [Nat.cast_succ]

Result:
case succ
α : Type u_1
inst✝ : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n) x
⊢ Commute (↑n + 1) x

Proof state:
α : Type u_1
inst✝ : NonAssocSemiring α
n : ℕ
x : α
⊢ Commute (↑n) x

Tactic:
induction n with
| zero => rw [Nat.cast_zero]; exact Commute.zero_left x
| succ n ihn => rw [Nat.cast_succ]; exact ihn.add_left (Commute.one_left x)

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n) x
⊢ Commute (↑n + 1) x

Tactic:
exact ihn.add_left (Commute.one_left x)

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝ : NonAssocSemiring α
x : α
⊢ Commute (↑0) x

Tactic:
rw [Nat.cast_zero]

Result:
case zero
α : Type u_1
inst✝ : NonAssocSemiring α
x : α
⊢ Commute 0 x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem signExtend_eq_setWidth_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
    x.signExtend v = x.setWidth v

Proof state:
case neg
w : Nat
x : BitVec w
v : Nat
hmsb : x.msb = false
i : Nat
a✝ : i < v
hv : ¬i < v
⊢ (signExtend v x).getLsbD i = false

Tactic:
apply getLsbD_ge

Result:
case neg.ge
w : Nat
x : BitVec w
v : Nat
hmsb : x.msb = false
i : Nat
a✝ : i < v
hv : ¬i < v
⊢ v ≤ i

Proof state:
case pos
w : Nat
x : BitVec w
v : Nat
hmsb : x.msb = false
i : Nat
a✝ hv : i < v
⊢ (signExtend v x).getLsbD i = (setWidth v x).getLsbD i

Tactic:
simp only [signExtend, getLsbD, getLsbD_setWidth, hv, decide_true, Bool.true_and, toNat_ofInt,
  BitVec.toInt_eq_msb_cond, hmsb, ↓reduceIte, reduceCtorEq]

Result:
case pos
w : Nat
x : BitVec w
v : Nat
hmsb : x.msb = false
i : Nat
a✝ hv : i < v
⊢ (↑x.toNat % ↑(2 ^ v)).toNat.testBit i = (setWidth v x).toNat.testBit i

Proof state:
w : Nat
x : BitVec w
v : Nat
hmsb : x.msb = false
⊢ signExtend v x = setWidth v x

Tactic:
ext i

Result:
case pred
w : Nat
x : BitVec w
v : Nat
hmsb : x.msb = false
i : Nat
a✝ : i < v
⊢ (signExtend v x).getLsbD i = (setWidth v x).getLsbD i

Proof state:
case pos
w : Nat
x : BitVec w
v : Nat
hmsb : x.msb = false
i : Nat
a✝ hv : i < v
⊢ (↑x.toNat % ↑(2 ^ v)).toNat.testBit i = (setWidth v x).toNat.testBit i

Tactic:
rw [Int.ofNat_mod_ofNat, Int.toNat_ofNat, Nat.testBit_mod_two_pow]

Result:
case pos
w : Nat
x : BitVec w
v : Nat
hmsb : x.msb = false
i : Nat
a✝ hv : i < v
⊢ (decide (i < v) && x.toNat.testBit i) = (setWidth v x).toNat.testBit i

Proof state:
case pos
w : Nat
x : BitVec w
v : Nat
hmsb : x.msb = false
i : Nat
a✝ hv : i < v
⊢ (decide (i < v) && x.toNat.testBit i) = (setWidth v x).toNat.testBit i

Tactic:
simp [BitVec.testBit_toNat]

Result:
no goals

Proof state:
case neg.ge
w : Nat
x : BitVec w
v : Nat
hmsb : x.msb = false
i : Nat
a✝ : i < v
hv : ¬i < v
⊢ v ≤ i

Tactic:
omega

Result:
no goals

Proof state:
case pred
w : Nat
x : BitVec w
v : Nat
hmsb : x.msb = false
i : Nat
a✝ : i < v
⊢ (signExtend v x).getLsbD i = (setWidth v x).getLsbD i

Tactic:
by_cases hv : i < v

Result:
case pos
w : Nat
x : BitVec w
v : Nat
hmsb : x.msb = false
i : Nat
a✝ hv : i < v
⊢ (signExtend v x).getLsbD i = (setWidth v x).getLsbD i

case neg
w : Nat
x : BitVec w
v : Nat
hmsb : x.msb = false
i : Nat
a✝ : i < v
hv : ¬i < v
⊢ (signExtend v x).getLsbD i = (setWidth v x).getLsbD i

Proof state:
case neg
w : Nat
x : BitVec w
v : Nat
hmsb : x.msb = false
i : Nat
a✝ : i < v
hv : ¬i < v
⊢ (signExtend v x).getLsbD i = (setWidth v x).getLsbD i

Tactic:
simp only [getLsbD_setWidth, hv, decide_false, Bool.false_and]

Result:
case neg
w : Nat
x : BitVec w
v : Nat
hmsb : x.msb = false
i : Nat
a✝ : i < v
hv : ¬i < v
⊢ (signExtend v x).getLsbD i = false
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem IsBilimit.binary_total {X Y : C} {b : BinaryBicone X Y} (i : b.IsBilimit) :
    b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt :=
  i.isLimit.hom_ext fun j => by rcases j with ⟨⟨⟩⟩ <;> simp

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
i : b.IsBilimit
j : Discrete WalkingPair
⊢ (b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ b.toCone.π.app j = 𝟙 b.pt ≫ b.toCone.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩ <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
lemma norm_eq_one_iff' : ‖x‖ = 1 ↔ ∃ θ ∈ Set.Ioc (-π) π, exp (θ * I) = x

Proof state:
case mpr.intro.intro
θ : ℝ
left✝ : θ ∈ Ioc (-π) π
⊢ ∃ θ_1, cexp (↑θ_1 * I) = cexp (↑θ * I)

Tactic:
exact ⟨θ, rfl⟩

Result:
no goals

Proof state:
x : ℂ
⊢ (∃ θ, cexp (↑θ * I) = x) ↔ ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x

Tactic:
constructor

Result:
case mp
x : ℂ
⊢ (∃ θ, cexp (↑θ * I) = x) → ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x

case mpr
x : ℂ
⊢ (∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x) → ∃ θ, cexp (↑θ * I) = x

Proof state:
x : ℂ
⊢ ‖x‖ = 1 ↔ ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x

Tactic:
rw [norm_eq_one_iff]

Result:
x : ℂ
⊢ (∃ θ, cexp (↑θ * I) = x) ↔ ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x

Proof state:
case h.e'_4.h.e'_4
θ : ℝ
⊢ π = -π + 2 * π

Tactic:
ring

Result:
no goals

Proof state:
case mp
x : ℂ
⊢ (∃ θ, cexp (↑θ * I) = x) → ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x

Tactic:
rintro ⟨θ, rfl⟩

Result:
case mp.intro
θ : ℝ
⊢ ∃ θ_1 ∈ Ioc (-π) π, cexp (↑θ_1 * I) = cexp (↑θ * I)

Proof state:
case mp.intro.refine_2
θ : ℝ
⊢ cexp (↑(toIocMod ⋯ (-π) θ) * I) = cexp (↑θ * I)

Tactic:
rw [eq_sub_of_add_eq <| toIocMod_add_toIocDiv_zsmul _ _ θ, ofReal_sub,
ofReal_zsmul, ofReal_mul, ofReal_ofNat, exp_mul_I_periodic.sub_zsmul_eq]

Result:
no goals

Proof state:
case mp.intro
θ : ℝ
⊢ ∃ θ_1 ∈ Ioc (-π) π, cexp (↑θ_1 * I) = cexp (↑θ * I)

Tactic:
refine ⟨toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ, ?_, ?_⟩

Result:
case mp.intro.refine_1
θ : ℝ
⊢ toIocMod ⋯ (-π) θ ∈ Ioc (-π) π

case mp.intro.refine_2
θ : ℝ
⊢ cexp (↑(toIocMod ⋯ (-π) θ) * I) = cexp (↑θ * I)

Proof state:
case mp.intro.refine_1
θ : ℝ
⊢ toIocMod ⋯ (-π) θ ∈ Ioc (-π) π

Tactic:
convert toIocMod_mem_Ioc _ _ _

Result:
case h.e'_4.h.e'_4
θ : ℝ
⊢ π = -π + 2 * π

Proof state:
case mpr
x : ℂ
⊢ (∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x) → ∃ θ, cexp (↑θ * I) = x

Tactic:
rintro ⟨θ, _, rfl⟩

Result:
case mpr.intro.intro
θ : ℝ
left✝ : θ ∈ Ioc (-π) π
⊢ ∃ θ_1, cexp (↑θ_1 * I) = cexp (↑θ * I)
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem oangle_add_right_eq_arccos_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    o.oangle x (x + y) = Real.arccos (‖x‖ / ‖x + y‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ o.oangle x (x + y) = ↑(Real.arccos (‖x‖ / ‖x + y‖))

Tactic:
have hs : (o.oangle x (x + y)).sign = 1 := by
  rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ o.oangle x (x + y) = ↑(Real.arccos (‖x‖ / ‖x + y‖))

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle x (x + y)).sign = 1

Tactic:
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ o.oangle x (x + y) = ↑(Real.arccos (‖x‖ / ‖x + y‖))

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs,
  InnerProductGeometry.angle_add_eq_arccos_of_inner_eq_zero
    (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Supported.lean
theorem X_mem_supported [Nontrivial R] {i : σ} : X i ∈ supported R s ↔ i ∈ s

Proof state:
σ : Type u_1
R : Type u
inst✝¹ : CommSemiring R
s : Set σ
inst✝ : Nontrivial R
i : σ
⊢ X i ∈ supported R s ↔ i ∈ s

Tactic:
simp [mem_supported]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem dist_eq_abs_sub_dist_iff_angle_eq_zero {p₁ p₂ p₃ : P} (hp₁p₂ : p₁ ≠ p₂) (hp₃p₂ : p₃ ≠ p₂) :
    dist p₁ p₃ = |dist p₁ p₂ - dist p₃ p₂| ↔ ∠ p₁ p₂ p₃ = 0

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
⊢ ‖p₁ -ᵥ ?p₃ - (p₃ -ᵥ ?p₃)‖ = |‖p₁ -ᵥ p₂‖ - ‖p₃ -ᵥ p₂‖| ↔ ∠ p₁ p₂ p₃ = 0

case p₃
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
⊢ P

Tactic:
exact
  norm_sub_eq_abs_sub_norm_iff_angle_eq_zero (fun he => hp₁p₂ (vsub_eq_zero_iff_eq.1 he))
    fun he => hp₃p₂ (vsub_eq_zero_iff_eq.1 he)

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
⊢ dist p₁ p₃ = |dist p₁ p₂ - dist p₃ p₂| ↔ ∠ p₁ p₂ p₃ = 0

Tactic:
rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
⊢ ‖p₁ -ᵥ ?p₃ - (p₃ -ᵥ ?p₃)‖ = |‖p₁ -ᵥ p₂‖ - ‖p₃ -ᵥ p₂‖| ↔ ∠ p₁ p₂ p₃ = 0

case p₃
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
⊢ P