harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem map_mapRange_eq_iff (f : R →+* S₁) (g : S₁ → R) (hg : g 0 = 0) (φ : MvPolynomial σ S₁) :
    map f (Finsupp.mapRange g hg φ) = φ ↔ ∀ d, f (g (coeff d φ)) = coeff d φ

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₁ → R
hg : g 0 = 0
φ : MvPolynomial σ S₁
⊢ (map f) (mapRange g hg φ) = φ ↔ ∀ (d : σ →₀ ℕ), f (g (coeff d φ)) = coeff d φ

Tactic:
rw [MvPolynomial.ext_iff]

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₁ → R
hg : g 0 = 0
φ : MvPolynomial σ S₁
⊢ (∀ (m : σ →₀ ℕ), coeff m ((map f) (mapRange g hg φ)) = coeff m φ) ↔ ∀ (d : σ →₀ ℕ), f (g (coeff d φ)) = coeff d φ

Proof state:
case h
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₁ → R
hg : g 0 = 0
φ : MvPolynomial σ S₁
m : σ →₀ ℕ
⊢ coeff m ((map f) (mapRange g hg φ)) = coeff m φ ↔ f (g (coeff m φ)) = coeff m φ

Tactic:
rw [coeff_map]

Result:
case h
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₁ → R
hg : g 0 = 0
φ : MvPolynomial σ S₁
m : σ →₀ ℕ
⊢ f (coeff m (mapRange g hg φ)) = coeff m φ ↔ f (g (coeff m φ)) = coeff m φ

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₁ → R
hg : g 0 = 0
φ : MvPolynomial σ S₁
⊢ (∀ (m : σ →₀ ℕ), coeff m ((map f) (mapRange g hg φ)) = coeff m φ) ↔ ∀ (d : σ →₀ ℕ), f (g (coeff d φ)) = coeff d φ

Tactic:
apply forall_congr'

Result:
case h
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₁ → R
hg : g 0 = 0
φ : MvPolynomial σ S₁
⊢ ∀ (a : σ →₀ ℕ), coeff a ((map f) (mapRange g hg φ)) = coeff a φ ↔ f (g (coeff a φ)) = coeff a φ

Proof state:
case h.a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₁ → R
hg : g 0 = 0
φ : MvPolynomial σ S₁
m : σ →₀ ℕ
⊢ f (coeff m (mapRange g hg φ)) = f (g (coeff m φ))

Tactic:
rfl

Result:
no goals

Proof state:
case h
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₁ → R
hg : g 0 = 0
φ : MvPolynomial σ S₁
⊢ ∀ (a : σ →₀ ℕ), coeff a ((map f) (mapRange g hg φ)) = coeff a φ ↔ f (g (coeff a φ)) = coeff a φ

Tactic:
intro m

Result:
case h
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₁ → R
hg : g 0 = 0
φ : MvPolynomial σ S₁
m : σ →₀ ℕ
⊢ coeff m ((map f) (mapRange g hg φ)) = coeff m φ ↔ f (g (coeff m φ)) = coeff m φ

Proof state:
case h
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₁ → R
hg : g 0 = 0
φ : MvPolynomial σ S₁
m : σ →₀ ℕ
⊢ f (coeff m (mapRange g hg φ)) = coeff m φ ↔ f (g (coeff m φ)) = coeff m φ

Tactic:
apply eq_iff_eq_cancel_right.mpr

Result:
case h.a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₁ → R
hg : g 0 = 0
φ : MvPolynomial σ S₁
m : σ →₀ ℕ
⊢ f (coeff m (mapRange g hg φ)) = f (g (coeff m φ))
-- Mathlib/GroupTheory/Coset/Defs.lean
theorem preimage_image_mk_eq_iUnion_image (N : Subgroup α) (s : Set α) :
    mk ⁻¹' ((mk : α → α ⧸ N) '' s) = ⋃ x : N, (· * (x : α)) '' s

Proof state:
α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
⊢ ∀ (x : ↥N), (fun x_1 => x_1 * ↑x⁻¹) '' s = (fun x_1 => x_1 * ↑x) ⁻¹' s

Tactic:
exact fun x ↦ image_mul_right'

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
lemma opcyclesMap_eq [S₁.HasRightHomology] [S₂.HasRightHomology] :
    opcyclesMap φ = h₁.opcyclesIso.hom ≫ γ.φQ ≫ h₂.opcyclesIso.inv

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ opcyclesMap φ = h₁.opcyclesIso.hom ≫ γ.φQ ≫ h₂.opcyclesIso.inv

Tactic:
dsimp [RightHomologyData.opcyclesIso, cyclesMapIso']

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ opcyclesMap φ = opcyclesMap' (𝟙 S₁) S₁.rightHomologyData h₁ ≫ γ.φQ ≫ opcyclesMap' (𝟙 S₂) h₂ S₂.rightHomologyData

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ opcyclesMap φ = opcyclesMap' (𝟙 S₁) S₁.rightHomologyData h₁ ≫ γ.φQ ≫ opcyclesMap' (𝟙 S₂) h₂ S₂.rightHomologyData

Tactic:
rw [← γ.opcyclesMap'_eq, ← opcyclesMap'_comp, ← opcyclesMap'_comp, id_comp, comp_id]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ opcyclesMap φ = opcyclesMap' φ S₁.rightHomologyData S₂.rightHomologyData

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ opcyclesMap φ = opcyclesMap' φ S₁.rightHomologyData S₂.rightHomologyData

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Basic.lean
@[to_additive (attr := simp)]
lemma comp_div (f : G →* H) (g h : M →* G) : f.comp (g / h) = f.comp g / f.comp h

Proof state:
case h
M : Type u_2
G : Type u_5
H : Type u_6
inst✝² : MulOneClass M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : G →* H
g h : M →* G
x✝ : M
⊢ (f.comp (g / h)) x✝ = (f.comp g / f.comp h) x✝

Tactic:
simp only [Function.comp_apply, div_apply, map_div, coe_comp]

Result:
no goals

Proof state:
M : Type u_2
G : Type u_5
H : Type u_6
inst✝² : MulOneClass M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : G →* H
g h : M →* G
⊢ f.comp (g / h) = f.comp g / f.comp h

Tactic:
ext

Result:
case h
M : Type u_2
G : Type u_5
H : Type u_6
inst✝² : MulOneClass M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : G →* H
g h : M →* G
x✝ : M
⊢ (f.comp (g / h)) x✝ = (f.comp g / f.comp h) x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem replicate_zero {x : BitVec w} : x.replicate 0 = 0#0

Proof state:
w : Nat
x : BitVec w
⊢ replicate 0 x = 0#0

Tactic:
simp [replicate]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem div_le_of_le_mul {a b c : Ordinal} (h : a ≤ b * c) : a / b ≤ c :=
  if b0 : b = 0 then by simp only [b0, div_zero, Ordinal.zero_le]
  else
    (div_le b0).2 <| h.trans_lt <| mul_lt_mul_of_pos_left (lt_succ c) (Ordinal.pos_iff_ne_zero.2 b0)

Proof state:
a b c : Ordinal.{u_4}
h : a ≤ b * c
b0 : b = 0
⊢ a / b ≤ c

Tactic:
simp only [b0, div_zero, Ordinal.zero_le]

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Basic.lean
theorem isThin_iff : Quiver.IsThin C ↔ ∀ c : C, Subsingleton (c ⟶ c)

Proof state:
C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton (d ⟶ d)
⊢ f = g

Tactic:
calc
  f = f ≫ inv g ≫ g := by simp only [inv_eq_inv, IsIso.inv_hom_id, Category.comp_id]
  _ = f ≫ inv f ≫ g := by congr 1
                          simp only [inv_eq_inv, IsIso.inv_hom_id, eq_iff_true_of_subsingleton]
  _ = g := by simp only [inv_eq_inv, IsIso.hom_inv_id_assoc]

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
⊢ f = g

Tactic:
haveI := h d

Result:
C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton (d ⟶ d)
⊢ f = g

Proof state:
C : Type u_1
inst✝ : Groupoid C
⊢ Quiver.IsThin C ↔ ∀ (c : C), Subsingleton (c ⟶ c)

Tactic:
refine ⟨fun h c => h c c, fun h c d => Subsingleton.intro fun f g => ?_⟩

Result:
C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
⊢ f = g

Proof state:
case e_a
C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton (d ⟶ d)
⊢ inv g ≫ g = inv f ≫ g

Tactic:
simp only [inv_eq_inv, IsIso.inv_hom_id, eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton (d ⟶ d)
⊢ f ≫ inv g ≫ g = f ≫ inv f ≫ g

Tactic:
congr 1

Result:
case e_a
C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton (d ⟶ d)
⊢ inv g ≫ g = inv f ≫ g

Proof state:
C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton (d ⟶ d)
⊢ f ≫ inv f ≫ g = g

Tactic:
simp only [inv_eq_inv, IsIso.hom_inv_id_assoc]

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton (d ⟶ d)
⊢ f = f ≫ inv g ≫ g

Tactic:
simp only [inv_eq_inv, IsIso.inv_hom_id, Category.comp_id]

Result:
no goals
-- Mathlib/Algebra/Category/Ring/Under/Limits.lean
lemma equalizer_comp {A B : Under R} (f g : A ⟶ B) :
    (AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder ≫ f =
    (AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder ≫ g

Proof state:
R : CommRingCat
A B : Under R
f g : A ⟶ B
⊢ (AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder ≫ f =
    (AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder ≫ g

Tactic:
ext (a : AlgHom.equalizer (toAlgHom f) (toAlgHom g))

Result:
case h
R : CommRingCat
A B : Under R
f g : A ⟶ B
a : ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))
⊢ (ConcreteCategory.hom ((AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder ≫ f).right) a =
    (ConcreteCategory.hom ((AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder ≫ g).right) a

Proof state:
case h
R : CommRingCat
A B : Under R
f g : A ⟶ B
a : ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))
⊢ (ConcreteCategory.hom ((AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder ≫ f).right) a =
    (ConcreteCategory.hom ((AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder ≫ g).right) a

Tactic:
exact a.property

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem measurableSet_region_between_cc (hf : Measurable f) (hg : Measurable g)
    (hs : MeasurableSet s) :
    MeasurableSet { p : α × ℝ | p.fst ∈ s ∧ p.snd ∈ Icc (f p.fst) (g p.fst) }

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Icc (f p.1) (g p.1)}

Tactic:
dsimp only [regionBetween, Icc, mem_setOf_eq, setOf_and]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet ({a | a.1 ∈ s} ∩ {a | a.2 ∈ {a_1 | f a.1 ≤ a_1} ∩ {a_1 | a_1 ≤ g a.1}})

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet ({a | a.1 ∈ s} ∩ {a | a.2 ∈ {a_1 | f a.1 ≤ a_1} ∩ {a_1 | a_1 ≤ g a.1}})

Tactic:
refine
  MeasurableSet.inter ?_
    ((measurableSet_le (hf.comp measurable_fst) measurable_snd).inter
      (measurableSet_le measurable_snd (hg.comp measurable_fst)))

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {a | a.1 ∈ s}

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {a | a.1 ∈ s}

Tactic:
exact measurable_fst hs

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem tsub_tsub (b a c : α) : b - a - c = b - (a + c)

Proof state:
case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - (a + c) ≤ b - a - c

Tactic:
rw [tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - a - c ≤ b - (a + c)

Tactic:
rw [tsub_le_iff_left, tsub_le_iff_left, ← add_assoc, ← tsub_le_iff_left]

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - a - c = b - (a + c)

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - a - c ≤ b - (a + c)

case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - (a + c) ≤ b - a - c
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
theorem swapRight_apply' (κ : Kernel α (β × γ)) (a : α) {s : Set (γ × β)} (hs : MeasurableSet s) :
    swapRight κ a s = κ a {p | p.swap ∈ s}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set (γ × β)
hs : MeasurableSet s
⊢ (κ.swapRight a) s = (κ a) {p | p.swap ∈ s}

Tactic:
rw [swapRight_apply, Measure.map_apply measurable_swap hs]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set (γ × β)
hs : MeasurableSet s
⊢ (κ a) (Prod.swap ⁻¹' s) = (κ a) {p | p.swap ∈ s}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set (γ × β)
hs : MeasurableSet s
⊢ (κ a) (Prod.swap ⁻¹' s) = (κ a) {p | p.swap ∈ s}

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
lemma SymmetricCategory.reverseBraiding_eq (C : Type u₁) [Category.{v₁} C]
    [MonoidalCategory C] [i : SymmetricCategory C] :
    reverseBraiding C = i.toBraidedCategory

Proof state:
case e_braiding
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
i : SymmetricCategory C
⊢ (fun X Y => (β_ Y X).symm) = β_

Tactic:
funext X Y

Result:
case e_braiding.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
i : SymmetricCategory C
X Y : C
⊢ (β_ Y X).symm = β_ X Y

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
i : SymmetricCategory C
⊢ { braiding := fun X Y => (β_ Y X).symm, braiding_naturality_right := ⋯, braiding_naturality_left := ⋯,
      hexagon_forward := ⋯, hexagon_reverse := ⋯ } =
    toBraidedCategory

Tactic:
congr

Result:
case e_braiding
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
i : SymmetricCategory C
⊢ (fun X Y => (β_ Y X).symm) = β_

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
i : SymmetricCategory C
⊢ reverseBraiding C = toBraidedCategory

Tactic:
dsimp only [reverseBraiding]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
i : SymmetricCategory C
⊢ { braiding := fun X Y => (β_ Y X).symm, braiding_naturality_right := ⋯, braiding_naturality_left := ⋯,
      hexagon_forward := ⋯, hexagon_reverse := ⋯ } =
    toBraidedCategory

Proof state:
case e_braiding.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
i : SymmetricCategory C
X Y : C
⊢ (β_ Y X).symm = β_ X Y

Tactic:
exact Iso.ext (braiding_swap_eq_inv_braiding Y X).symm

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftedHom.lean
lemma comp_mk₀ {a : M} (f : ShiftedHom X Y a) (m₀ : M) (hm₀ : m₀ = 0) (g : Y ⟶ Z) :
    f.comp (mk₀ m₀ hm₀ g) (by rw [hm₀, zero_add]) = f ≫ g⟦a⟧'

Proof state:
C : Type u_1
inst✝⁶ : Category.{?u.21100, u_1} C
D : Type u_2
inst✝⁵ : Category.{?u.21107, u_2} D
E : Type u_3
inst✝⁴ : Category.{?u.21114, u_3} E
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
inst✝ : HasShift E M
X Y Z T : C
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
g : Y ⟶ Z
⊢ m₀ + a = a

Tactic:
rw [hm₀, zero_add]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
a : M
f : ShiftedHom X Y a
g : Y ⟶ Z
⊢ f.comp (mk₀ 0 ⋯ g) ⋯ = f ≫ (shiftFunctor C a).map g

Tactic:
simp only [comp, shiftFunctorAdd'_zero_add_inv_app, mk₀, shiftFunctorZero',
  eqToIso_refl, Iso.refl_trans, ← Functor.map_comp, assoc, Iso.inv_hom_id_app,
  Functor.id_obj, comp_id]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
g : Y ⟶ Z
⊢ f.comp (mk₀ m₀ hm₀ g) ⋯ = f ≫ (shiftFunctor C a).map g

Tactic:
subst hm₀

Result:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
a : M
f : ShiftedHom X Y a
g : Y ⟶ Z
⊢ f.comp (mk₀ 0 ⋯ g) ⋯ = f ≫ (shiftFunctor C a).map g
-- Mathlib/Algebra/Module/LocalizedModule/Submodule.lean
lemma range_localizedMap_eq_localized₀_range (g : M →ₗ[R] P) :
    range (map p f f' g) = (range g).localized₀ p f'

Proof state:
case h
R : Type u_1
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝⁵ : IsLocalizedModule p f
P : Type u_5
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
Q : Type u_6
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
x✝ : Q
⊢ x✝ ∈ range ((IsLocalizedModule.map p f f') g) ↔ x✝ ∈ localized₀ p f' (range g)

Tactic:
simp [mem_localized₀, mem_range, (mk'_surjective p f).exists]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝⁵ : IsLocalizedModule p f
P : Type u_5
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
Q : Type u_6
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
⊢ range ((IsLocalizedModule.map p f f') g) = localized₀ p f' (range g)

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝⁵ : IsLocalizedModule p f
P : Type u_5
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
Q : Type u_6
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
x✝ : Q
⊢ x✝ ∈ range ((IsLocalizedModule.map p f f') g) ↔ x✝ ∈ localized₀ p f' (range g)
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem join₂_map (f : R →+* MvPolynomial σ S) (φ : MvPolynomial σ R) :
    join₂ (map f φ) = bind₂ f φ

Proof state:
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* MvPolynomial σ S
φ : MvPolynomial σ R
⊢ join₂ ((map f) φ) = (bind₂ f) φ

Tactic:
simp only [join₂, bind₂, eval₂Hom_map_hom, RingHom.id_comp]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C'
    (hx : AlgebraicIndependent R x) (r) :
    Polynomial.C (hx.aevalEquiv (C r)) = Polynomial.C (algebraMap _ _ r)

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
r : R
⊢ Polynomial.C (hx.aevalEquiv (C r)) = Polynomial.C ((algebraMap R ↥(adjoin R (range x))) r)

Tactic:
congr

Result:
case h.e_6.h
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
r : R
⊢ hx.aevalEquiv (C r) = (algebraMap R ↥(adjoin R (range x))) r

Proof state:
case h.e_6.h
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
r : R
⊢ hx.aevalEquiv (C r) = (algebraMap R ↥(adjoin R (range x))) r

Tactic:
apply_fun Subtype.val using Subtype.val_injective

Result:
case h.e_6.h
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
r : R
⊢ ↑(hx.aevalEquiv (C r)) = ↑((algebraMap R ↥(adjoin R (range x))) r)

Proof state:
case h.e_6.h
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
r : R
⊢ ↑(hx.aevalEquiv (C r)) = ↑((algebraMap R ↥(adjoin R (range x))) r)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem generate (B : FilterBasis α) : generate B.sets = B.filter

Proof state:
case a.intro.intro
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.filter
V : Set α
V_in : V ∈ B
h : V ⊆ U
⊢ U ∈ generate B.sets

Tactic:
exact GenerateSets.superset (GenerateSets.basic V_in) h

Result:
no goals

Proof state:
case a
α : Type u_1
B : FilterBasis α
⊢ generate B.sets ≤ B.filter

Tactic:
intro U U_in

Result:
case a
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.filter
⊢ U ∈ generate B.sets

Proof state:
α : Type u_1
B : FilterBasis α
⊢ generate B.sets = B.filter

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
B : FilterBasis α
⊢ generate B.sets ≤ B.filter

case a
α : Type u_1
B : FilterBasis α
⊢ B.filter ≤ generate B.sets

Proof state:
case a
α : Type u_1
B : FilterBasis α
⊢ B.filter ≤ generate B.sets

Tactic:
rw [le_generate_iff]

Result:
case a
α : Type u_1
B : FilterBasis α
⊢ B.sets ⊆ B.filter.sets

Proof state:
case a
α : Type u_1
B : FilterBasis α
⊢ B.sets ⊆ B.filter.sets

Tactic:
apply mem_filter_of_mem

Result:
no goals

Proof state:
case a
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.filter
⊢ U ∈ generate B.sets

Tactic:
rcases B.mem_filter_iff.mp U_in with ⟨V, V_in, h⟩

Result:
case a.intro.intro
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.filter
V : Set α
V_in : V ∈ B
h : V ⊆ U
⊢ U ∈ generate B.sets
-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
lemma ΓSpecIso_inv_ΓSpec_adjunction_homEquiv {X : Scheme.{u}} {B : CommRingCat} (φ : B ⟶ Γ(X, ⊤)) :
    (Scheme.ΓSpecIso B).inv ≫ ((ΓSpec.adjunction.homEquiv X (op B)) φ.op).appTop = φ

Proof state:
X : Scheme
B : CommRingCat
φ : B ⟶ Γ(X, ⊤)
⊢ (Scheme.ΓSpecIso B).inv ≫ Scheme.Hom.appTop ((ΓSpec.adjunction.homEquiv X (op B)) φ.op) = φ

Tactic:
simp only [Adjunction.homEquiv_apply, Scheme.Spec_map, Opens.map_top, Scheme.comp_app]

Result:
X : Scheme
B : CommRingCat
φ : B ⟶ Γ(X, ⊤)
⊢ (Scheme.ΓSpecIso B).inv ≫ Scheme.Hom.app (Spec.map φ.op.unop) ⊤ ≫ Scheme.Hom.app (ΓSpec.adjunction.unit.app X) ⊤ = φ

Proof state:
X : Scheme
B : CommRingCat
φ : B ⟶ Γ(X, ⊤)
⊢ (Scheme.ΓSpecIso B).inv ≫ Scheme.Hom.app (Spec.map φ.op.unop) ⊤ ≫ Scheme.Hom.app (ΓSpec.adjunction.unit.app X) ⊤ = φ

Tactic:
simp

Result:
no goals