harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma tilted_tilted (hf : Integrable (fun x ↦ exp (f x)) μ) (g : α → ℝ) :
    (μ.tilted f).tilted g = μ.tilted (f + g)

Proof state:
case inr.h.e_f.h.e_r
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
x : α
⊢ rexp (f x) * (rexp (g x) * ∫ (x : α), rexp (f x) ∂μ) / ((∫ (x : α), rexp (f x) ∂μ) * ∫ (x : α), rexp (f x + g x) ∂μ) =
    rexp (f x) * rexp (g x) / ∫ (x : α), rexp (f x + g x) ∂μ

Tactic:
ring_nf

Result:
case inr.h.e_f.h.e_r
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
x : α
⊢ (rexp (f x) * rexp (g x) * ∫ (x : α), rexp (f x) ∂μ) * (∫ (x : α), rexp (f x) ∂μ)⁻¹ *
      (∫ (x : α), rexp (f x + g x) ∂μ)⁻¹ =
    rexp (f x) * rexp (g x) * (∫ (x : α), rexp (f x + g x) ∂μ)⁻¹

Proof state:
case inr.h.e_f.h.e_r.e_a
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
x : α
⊢ ∫ (x : α), rexp (f x) ∂μ ≠ 0

Tactic:
exact (integral_exp_pos hf).ne'

Result:
no goals

Proof state:
case inr.h.e_f.h.e_r.e_a
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
x : α
⊢ (rexp (f x) * rexp (g x) * ∫ (x : α), rexp (f x) ∂μ) * (∫ (x : α), rexp (f x) ∂μ)⁻¹ = rexp (f x) * rexp (g x)

Tactic:
rw [mul_assoc, mul_inv_cancel₀, mul_one]

Result:
case inr.h.e_f.h.e_r.e_a
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
x : α
⊢ ∫ (x : α), rexp (f x) ∂μ ≠ 0
-- Mathlib/Combinatorics/SetFamily/Intersecting.lean
theorem intersecting_iff_eq_empty_of_subsingleton [Subsingleton α] (s : Set α) :
    s.Intersecting ↔ s = ∅

Proof state:
case refine_1
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : Subsingleton α
s : Set α
h : ¬s = ∅
⊢ ⊥ ∈ s

Tactic:
obtain ⟨a, ha⟩ := nonempty_iff_ne_empty.2 h

Result:
case refine_1.intro
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : Subsingleton α
s : Set α
h : ¬s = ∅
a : α
ha : a ∈ s
⊢ ⊥ ∈ s

Proof state:
case refine_2
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : Subsingleton α
s : Set α
⊢ s = ∅ → s ≠ {⊥}

Tactic:
rintro rfl

Result:
case refine_2
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : Subsingleton α
⊢ ∅ ≠ {⊥}

Proof state:
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : Subsingleton α
s : Set α
⊢ s.Intersecting ↔ s = ∅

Tactic:
refine
  subsingleton_of_subsingleton.intersecting.trans
    ⟨not_imp_comm.2 fun h => subsingleton_of_subsingleton.eq_singleton_of_mem ?_, ?_⟩

Result:
case refine_1
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : Subsingleton α
s : Set α
h : ¬s = ∅
⊢ ⊥ ∈ s

case refine_2
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : Subsingleton α
s : Set α
⊢ s = ∅ → s ≠ {⊥}

Proof state:
case refine_1.intro
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : Subsingleton α
s : Set α
h : ¬s = ∅
a : α
ha : a ∈ s
⊢ ⊥ ∈ s

Tactic:
rwa [Subsingleton.elim ⊥ a]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : Subsingleton α
⊢ ∅ ≠ {⊥}

Tactic:
exact (Set.singleton_nonempty _).ne_empty.symm

Result:
no goals
-- Mathlib/Algebra/AddTorsor/Defs.lean
theorem neg_vsub_eq_vsub_rev (p₁ p₂ : P) : -(p₁ -ᵥ p₂) = p₂ -ᵥ p₁

Proof state:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
⊢ (p₁ -ᵥ p₂ + (p₂ -ᵥ p₁)) +ᵥ p₁ = 0 +ᵥ p₁

Tactic:
rw [vsub_add_vsub_cancel, vsub_self]

Result:
no goals

Proof state:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
⊢ -(p₁ -ᵥ p₂) = p₂ -ᵥ p₁

Tactic:
refine neg_eq_of_add_eq_zero_right (vadd_right_cancel p₁ ?_)

Result:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
⊢ (p₁ -ᵥ p₂ + (p₂ -ᵥ p₁)) +ᵥ p₁ = 0 +ᵥ p₁
-- Mathlib/CategoryTheory/Sites/Coherent/ExtensiveSheaves.lean
theorem isSheafFor_extensive_of_preservesFiniteProducts {X : C} (S : Presieve X) [S.Extensive]
    (F : Cᵒᵖ ⥤ Type w) [PreservesFiniteProducts F] : S.IsSheafFor F

Proof state:
case intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : FinitaryPreExtensive C
X : C
F : Cᵒᵖ ⥤ Type w
inst✝¹ : PreservesFiniteProducts F
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
inst✝ : (ofArrows Z π).Extensive
hc : IsColimit (Cofan.mk X π)
⊢ IsSheafFor F (ofArrows Z π)

Tactic:
have : (ofArrows Z (Cofan.mk X π).inj).hasPullbacks :=
  (inferInstance : (ofArrows Z π).hasPullbacks)

Result:
case intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : FinitaryPreExtensive C
X : C
F : Cᵒᵖ ⥤ Type w
inst✝¹ : PreservesFiniteProducts F
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
inst✝ : (ofArrows Z π).Extensive
hc : IsColimit (Cofan.mk X π)
this : (ofArrows Z (Cofan.mk X π).inj).hasPullbacks
⊢ IsSheafFor F (ofArrows Z π)

Proof state:
case intro.intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : FinitaryPreExtensive C
X : C
F : Cᵒᵖ ⥤ Type w
inst✝¹ : PreservesFiniteProducts F
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
inst✝ : (ofArrows Z π).Extensive
hc : IsColimit (Cofan.mk X π)
this : (ofArrows Z (Cofan.mk X π).inj).hasPullbacks
val✝ : Fintype α
⊢ IsSheafFor F (ofArrows Z π)

Tactic:
exact isSheafFor_of_preservesProduct _ _ hc

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : FinitaryPreExtensive C
X : C
F : Cᵒᵖ ⥤ Type w
inst✝¹ : PreservesFiniteProducts F
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
inst✝ : (ofArrows Z π).Extensive
hc : IsColimit (Cofan.mk X π)
this : (ofArrows Z (Cofan.mk X π).inj).hasPullbacks
⊢ IsSheafFor F (ofArrows Z π)

Tactic:
cases nonempty_fintype α

Result:
case intro.intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : FinitaryPreExtensive C
X : C
F : Cᵒᵖ ⥤ Type w
inst✝¹ : PreservesFiniteProducts F
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
inst✝ : (ofArrows Z π).Extensive
hc : IsColimit (Cofan.mk X π)
this : (ofArrows Z (Cofan.mk X π).inj).hasPullbacks
val✝ : Fintype α
⊢ IsSheafFor F (ofArrows Z π)

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : FinitaryPreExtensive C
X : C
S : Presieve X
inst✝¹ : S.Extensive
F : Cᵒᵖ ⥤ Type w
inst✝ : PreservesFiniteProducts F
⊢ IsSheafFor F S

Tactic:
obtain ⟨α, _, Z, π, rfl, ⟨hc⟩⟩ := Extensive.arrows_nonempty_isColimit (R := S)

Result:
case intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : FinitaryPreExtensive C
X : C
F : Cᵒᵖ ⥤ Type w
inst✝¹ : PreservesFiniteProducts F
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
inst✝ : (ofArrows Z π).Extensive
hc : IsColimit (Cofan.mk X π)
⊢ IsSheafFor F (ofArrows Z π)
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
theorem conj_smul_le_of_le {P H : Subgroup G} (hP : P ≤ H) (h : H) :
    MulAut.conj (h : G) • P ≤ H

Proof state:
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ MulAut.conj ↑h • P ≤ H

Tactic:
rintro - ⟨g, hg, rfl⟩

Result:
case intro.intro
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
g : G
hg : g ∈ ↑P
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj ↑h)) g ∈ H

Proof state:
case intro.intro
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
g : G
hg : g ∈ ↑P
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj ↑h)) g ∈ H

Tactic:
exact H.mul_mem (H.mul_mem h.2 (hP hg)) (H.inv_mem h.2)

Result:
no goals
-- Mathlib/MeasureTheory/PiSystem.lean
theorem piiUnionInter_singleton (π : ι → Set (Set α)) (i : ι) :
    piiUnionInter π {i} = π i ∪ {univ}

Proof state:
case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∈ t
ht_eq_i : t = {i}
⊢ ⋂ x ∈ t, f x ∈ π i ∨ ⋂ x ∈ t, f x ∈ {univ}

Tactic:
simp only [ht_eq_i, Finset.mem_singleton, iInter_iInter_eq_left]

Result:
case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∈ t
ht_eq_i : t = {i}
⊢ f i ∈ π i ∨ f i ∈ {univ}

Proof state:
case h.refine_2
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
h : s ∈ π i ∨ s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}

Tactic:
rcases h with hs | hs

Result:
case h.refine_2.inl
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}

case h.refine_2.inr
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}

Proof state:
case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
⊢ ⋂ x ∈ t, f x ∈ π i ∨ ⋂ x ∈ t, f x ∈ {univ}

Tactic:
have ht_empty : t = ∅ := by
  ext1 x
  simp only [Finset.not_mem_empty, iff_false]
  exact fun hx => hi (hti x hx ▸ hx)

Result:
case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
ht_empty : t = ∅
⊢ ⋂ x ∈ t, f x ∈ π i ∨ ⋂ x ∈ t, f x ∈ {univ}

Proof state:
case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
ht_empty : t = ∅
⊢ ⋂ x ∈ t, f x ∈ π i ∨ ⋂ x ∈ t, f x ∈ {univ}

Tactic:
simp [ht_empty, iInter_false, iInter_univ, Set.mem_singleton univ]

Result:
no goals

Proof state:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
⊢ t = ∅

Tactic:
ext1 x

Result:
case h
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
x : ι
⊢ x ∈ t ↔ x ∈ ∅
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem iteratedDerivWithin_univ : iteratedDerivWithin n f univ = iteratedDeriv n f

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedDerivWithin n f univ = iteratedDeriv n f

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ iteratedDerivWithin n f univ x = iteratedDeriv n f x

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ iteratedDerivWithin n f univ x = iteratedDeriv n f x

Tactic:
rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_univ]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
theorem Lp.induction_stronglyMeasurable (hm : m ≤ m0) (hp_ne_top : p ≠ ∞) (P : Lp F p μ → Prop)
    (h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet[m] s) (hμs : μ s < ∞),
      P (Lp.simpleFunc.indicatorConst p (hm s hs) hμs.ne c))
    (h_add : ∀ ⦃f g⦄, ∀ hf : MemLp f p μ, ∀ hg : MemLp g p μ, StronglyMeasurable[m] f →
      StronglyMeasurable[m] g → Disjoint (Function.support f) (Function.support g) →
        P (hf.toLp f) → P (hg.toLp g) → P (hf.toLp f + hg.toLp g))
    (h_closed : IsClosed {f : lpMeas F ℝ m p μ | P f}) :
    ∀ f : Lp F p μ, AEStronglyMeasurable[m] f μ → P f

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ⊤
P : ↥(Lp F p μ) → Prop
h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed {f | P ↑f}
f✝ : ↥(Lp F p μ)
hf✝ : AEStronglyMeasurable (↑↑f✝) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)

Tactic:
let s_g : Set α := Function.support (hgm.mk g)

Result:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ⊤
P : ↥(Lp F p μ) → Prop
h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed {f | P ↑f}
f✝ : ↥(Lp F p μ)
hf✝ : AEStronglyMeasurable (↑↑f✝) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)
-- Mathlib/Analysis/CStarAlgebra/Basic.lean
theorem norm_self_mul_star {x : E} : ‖x * x⋆‖ = ‖x‖ * ‖x‖

Proof state:
E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x⋆⋆ * x⋆‖ = ‖x‖ * ‖x‖

Tactic:
simp only [norm_star_mul_self, norm_star]

Result:
no goals

Proof state:
E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x * x⋆‖ = ‖x‖ * ‖x‖

Tactic:
nth_rw 1 [← star_star x]

Result:
E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x⋆⋆ * x⋆‖ = ‖x‖ * ‖x‖
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem one_right_iff : IsPrimitiveRoot ζ 1 ↔ ζ = 1

Proof state:
case mp
M : Type u_1
inst✝ : CommMonoid M
ζ : M
⊢ IsPrimitiveRoot ζ 1 → ζ = 1

Tactic:
intro h

Result:
case mp
M : Type u_1
inst✝ : CommMonoid M
ζ : M
h : IsPrimitiveRoot ζ 1
⊢ ζ = 1

Proof state:
case mpr
M : Type u_1
inst✝ : CommMonoid M
⊢ IsPrimitiveRoot 1 1

Tactic:
exact one

Result:
no goals

Proof state:
case mp
M : Type u_1
inst✝ : CommMonoid M
ζ : M
h : IsPrimitiveRoot ζ 1
⊢ ζ = 1

Tactic:
rw [← pow_one ζ, h.pow_eq_one]

Result:
no goals

Proof state:
case mpr
M : Type u_1
inst✝ : CommMonoid M
ζ : M
⊢ ζ = 1 → IsPrimitiveRoot ζ 1

Tactic:
rintro rfl

Result:
case mpr
M : Type u_1
inst✝ : CommMonoid M
⊢ IsPrimitiveRoot 1 1

Proof state:
M : Type u_1
inst✝ : CommMonoid M
ζ : M
⊢ IsPrimitiveRoot ζ 1 ↔ ζ = 1

Tactic:
constructor

Result:
case mp
M : Type u_1
inst✝ : CommMonoid M
ζ : M
⊢ IsPrimitiveRoot ζ 1 → ζ = 1

case mpr
M : Type u_1
inst✝ : CommMonoid M
ζ : M
⊢ ζ = 1 → IsPrimitiveRoot ζ 1
-- Mathlib/Data/Set/Card.lean
theorem Nat.card_coe_set_eq (s : Set α) : Nat.card s = s.ncard

Proof state:
case inl
α : Type u_1
s : Set α
h : s.Finite
this : Fintype ↑s
⊢ Nat.card ↑s = s.ncard

Tactic:
rw [ncard, h.encard_eq_coe_toFinset_card, Nat.card_eq_fintype_card,
  toFinite_toFinset, toFinset_card, ENat.toNat_coe]

Result:
no goals

Proof state:
case inr
α : Type u_1
s : Set α
h : s.Infinite
⊢ Nat.card ↑s = s.ncard

Tactic:
have := infinite_coe_iff.2 h

Result:
case inr
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ Nat.card ↑s = s.ncard

Proof state:
case inr
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ Nat.card ↑s = s.ncard

Tactic:
rw [ncard, h.encard_eq, Nat.card_eq_zero_of_infinite, ENat.toNat_top]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
⊢ Nat.card ↑s = s.ncard

Tactic:
obtain (h | h) := s.finite_or_infinite

Result:
case inl
α : Type u_1
s : Set α
h : s.Finite
⊢ Nat.card ↑s = s.ncard

case inr
α : Type u_1
s : Set α
h : s.Infinite
⊢ Nat.card ↑s = s.ncard

Proof state:
case inl
α : Type u_1
s : Set α
h : s.Finite
⊢ Nat.card ↑s = s.ncard

Tactic:
have := h.fintype

Result:
case inl
α : Type u_1
s : Set α
h : s.Finite
this : Fintype ↑s
⊢ Nat.card ↑s = s.ncard
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
@[simp] lemma mu_self (a : α) : mu 𝕜 a a = 1

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a : α
⊢ (mu 𝕜) a a = 1

Tactic:
simp [mu_apply]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem isOpen_extend_preimage {s : Set E} (hs : IsOpen s) :
    IsOpen (f.source ∩ f.extend I ⁻¹' s)

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 E
hs : IsOpen s
⊢ IsOpen (f.source ∩ ↑(f.extend I) ⁻¹' s)

Tactic:
rw [← extend_source f (I := 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 E
hs : IsOpen s
⊢ IsOpen ((f.extend I).source ∩ ↑(f.extend I) ⁻¹' s)

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 E
hs : IsOpen s
⊢ IsOpen ((f.extend I).source ∩ ↑(f.extend I) ⁻¹' s)

Tactic:
exact isOpen_extend_preimage' f hs

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/MvPolynomial.lean
theorem det_mvPolynomialX_ne_zero [DecidableEq m] [Fintype m] [CommRing R] [Nontrivial R] :
    det (mvPolynomialX m m R) ≠ 0

Proof state:
m : Type u_1
R : Type u_3
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ (mvPolynomialX m m R).det ≠ 0

Tactic:
intro h_det

Result:
m : Type u_1
R : Type u_3
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : (mvPolynomialX m m R).det = 0
⊢ False

Proof state:
m : Type u_1
R : Type u_3
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : (mvPolynomialX m m R).det = 0
this : ((MvPolynomial.eval fun p => 1 p.1 p.2).mapMatrix (mvPolynomialX m m R)).det = det 1
⊢ False

Tactic:
rw [det_one, ← RingHom.map_det, h_det, RingHom.map_zero] at this

Result:
m : Type u_1
R : Type u_3
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : (mvPolynomialX m m R).det = 0
this : 0 = 1
⊢ False

Proof state:
m : Type u_1
R : Type u_3
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : (mvPolynomialX m m R).det = 0
⊢ False

Tactic:
have := congr_arg Matrix.det (mvPolynomialX_mapMatrix_eval (1 : Matrix m m R))

Result:
m : Type u_1
R : Type u_3
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : (mvPolynomialX m m R).det = 0
this : ((MvPolynomial.eval fun p => 1 p.1 p.2).mapMatrix (mvPolynomialX m m R)).det = det 1
⊢ False

Proof state:
m : Type u_1
R : Type u_3
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : (mvPolynomialX m m R).det = 0
this : 0 = 1
⊢ False

Tactic:
exact zero_ne_one this

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem map_id (γ : Path x y) : γ.map continuous_id = γ

Proof state:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
x✝ : ↑I
⊢ (γ.map ⋯) x✝ = γ x✝

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ γ.map ⋯ = γ

Tactic:
ext

Result:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
x✝ : ↑I
⊢ (γ.map ⋯) x✝ = γ x✝
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem sign_prodExtendRight (a : α) (σ : Perm β) : sign (prodExtendRight a σ) = sign σ :=
  sign_bij (fun (ab : α × β) _ => ab.snd)
    (fun ⟨a', b⟩ hab _ => by simp [eq_of_prodExtendRight_ne hab])
    (fun ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ hab₁ hab₂ h => by
      simpa [eq_of_prodExtendRight_ne hab₁, eq_of_prodExtendRight_ne hab₂] using h)
    fun y hy => ⟨(a, y), by simpa, by simp⟩

Proof state:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
a : α
σ : Perm β
x✝¹ x✝ : α × β
a₁ : α
b₁ : β
hab₁ : (prodExtendRight a σ) (a₁, b₁) ≠ (a₁, b₁)
a₂ : α
b₂ : β
hab₂ : (prodExtendRight a σ) (a₂, b₂) ≠ (a₂, b₂)
h : (fun ab x => ab.2) (a₁, b₁) hab₁ = (fun ab x => ab.2) (a₂, b₂) hab₂
⊢ (a₁, b₁) = (a₂, b₂)

Tactic:
simpa [eq_of_prodExtendRight_ne hab₁, eq_of_prodExtendRight_ne hab₂] using h

Result:
no goals

Proof state:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
a : α
σ : Perm β
y : β
hy : σ y ≠ y
⊢ (prodExtendRight a σ) (a, y) ≠ (a, y)

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
a : α
σ : Perm β
x✝¹ : α × β
a' : α
b : β
hab : (prodExtendRight a σ) (a', b) ≠ (a', b)
x✝ : (prodExtendRight a σ) ((prodExtendRight a σ) (a', b)) ≠ (prodExtendRight a σ) (a', b)
⊢ (fun ab x => ab.2) ((prodExtendRight a σ) (a', b)) x✝ = σ ((fun ab x => ab.2) (a', b) hab)

Tactic:
simp [eq_of_prodExtendRight_ne hab]

Result:
no goals

Proof state:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
a : α
σ : Perm β
y : β
hy : σ y ≠ y
⊢ (fun ab x => ab.2) (a, y) ⋯ = y

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/ClassNumber/Finite.lean
theorem mem_finsetApprox {x : R} :
    x ∈ finsetApprox bS adm ↔ ∃ i j, i ≠ j ∧ distinctElems bS adm i - distinctElems bS adm j =
    x

Proof state:
case mpr.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
i j : Fin (cardM bS adm).succ
hij : i ≠ j
⊢ ¬(distinctElems bS adm) i = (distinctElems bS adm) j

Tactic:
exact fun h => hij ((distinctElems bS adm).injective h)

Result:
no goals

Proof state:
case mp.intro.intro.mk.intro
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
i j : Fin (cardM bS adm).succ
left✝ : (i, j) ∈ Finset.univ
hx : (distinctElems bS adm) (i, j).1 - (distinctElems bS adm) (i, j).2 ≠ 0
⊢ ∃ i_1 j_1,
    i_1 ≠ j_1 ∧
      (distinctElems bS adm) i_1 - (distinctElems bS adm) j_1 =
        (distinctElems bS adm) (i, j).1 - (distinctElems bS adm) (i, j).2

Tactic:
refine ⟨i, j, ?_, rfl⟩

Result:
case mp.intro.intro.mk.intro
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
i j : Fin (cardM bS adm).succ
left✝ : (i, j) ∈ Finset.univ
hx : (distinctElems bS adm) (i, j).1 - (distinctElems bS adm) (i, j).2 ≠ 0
⊢ i ≠ j