harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/ModelTheory/PartialEquiv.lean
theorem toEmbeddingOfEqTop_apply {f : M ≃ₚ[L] N} (h : f.dom = ⊤) (m : M) :
    toEmbeddingOfEqTop h m = f.toEquiv ⟨m, h.symm ▸ mem_top m⟩

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
h : f.dom = ⊤
m : M
⊢ (toEmbeddingOfEqTop h) m = ↑(f.toEquiv ⟨m, ⋯⟩)

Tactic:
rcases f with ⟨dom, cod, g⟩

Result:
case mk
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
m : M
dom : L.Substructure M
cod : L.Substructure N
g : ↥dom ≃[L] ↥cod
h : { dom := dom, cod := cod, toEquiv := g }.dom = ⊤
⊢ (toEmbeddingOfEqTop h) m = ↑({ dom := dom, cod := cod, toEquiv := g }.toEquiv ⟨m, ⋯⟩)

Proof state:
case mk.refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
m : M
cod : L.Substructure N
g : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod
⊢ (toEmbeddingOfEqTop ⋯) m =
    ↑({ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := g }.toEquiv ⟨m, ⋯⟩)

Tactic:
rfl

Result:
no goals

Proof state:
case mk
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
m : M
dom : L.Substructure M
cod : L.Substructure N
g : ↥dom ≃[L] ↥cod
h : { dom := dom, cod := cod, toEquiv := g }.dom = ⊤
⊢ (toEmbeddingOfEqTop h) m = ↑({ dom := dom, cod := cod, toEquiv := g }.toEquiv ⟨m, ⋯⟩)

Tactic:
cases h

Result:
case mk.refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
m : M
cod : L.Substructure N
g : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod
⊢ (toEmbeddingOfEqTop ⋯) m =
    ↑({ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := g }.toEquiv ⟨m, ⋯⟩)
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Represents.lean
lemma existsUnique_rep (hrep : Represents s C) (h : c ∈ C) : ∃! x, x ∈ s ∩ c.supp

Proof state:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ ∃! x, x ∈ s ∩ c.supp

Tactic:
obtain ⟨x, ⟨hx, rfl⟩⟩ := hrep.2.2 h

Result:
case intro.intro
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
hrep : Represents s C
x : V
hx : x ∈ s
h : G.connectedComponentMk x ∈ C
⊢ ∃! x_1, x_1 ∈ s ∩ (G.connectedComponentMk x).supp

Proof state:
case h
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
hrep : Represents s C
x : V
hx : x ∈ s
h : G.connectedComponentMk x ∈ C
⊢ ∀ y ∈ s, G.connectedComponentMk y = G.connectedComponentMk x → y = x

Tactic:
exact fun y hy hyx ↦ hrep.2.1 hy hx hyx

Result:
no goals

Proof state:
case intro.intro
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
hrep : Represents s C
x : V
hx : x ∈ s
h : G.connectedComponentMk x ∈ C
⊢ ∃! x_1, x_1 ∈ s ∩ (G.connectedComponentMk x).supp

Tactic:
use x

Result:
case h
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
hrep : Represents s C
x : V
hx : x ∈ s
h : G.connectedComponentMk x ∈ C
⊢ (fun x_1 => x_1 ∈ s ∩ (G.connectedComponentMk x).supp) x ∧
    ∀ (y : V), (fun x_1 => x_1 ∈ s ∩ (G.connectedComponentMk x).supp) y → y = x

Proof state:
case h
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
hrep : Represents s C
x : V
hx : x ∈ s
h : G.connectedComponentMk x ∈ C
⊢ (fun x_1 => x_1 ∈ s ∩ (G.connectedComponentMk x).supp) x ∧
    ∀ (y : V), (fun x_1 => x_1 ∈ s ∩ (G.connectedComponentMk x).supp) y → y = x

Tactic:
simp only [Set.mem_inter_iff, hx, SetLike.mem_coe, mem_supp_iff, and_self, and_imp, true_and]

Result:
case h
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
hrep : Represents s C
x : V
hx : x ∈ s
h : G.connectedComponentMk x ∈ C
⊢ ∀ y ∈ s, G.connectedComponentMk y = G.connectedComponentMk x → y = x
-- Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
lemma isLE_iff (n : ℤ) :
    K.IsLE n ↔ ∀ (i : ℤ) (_ : n < i), K.ExactAt i

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ (∀ (i : ℤ), n < i → ExactAt K i) → K.IsLE n

Tactic:
intro h

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → ExactAt K i
⊢ K.IsLE n

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsLE n ↔ ∀ (i : ℤ), n < i → ExactAt K i

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsLE n → ∀ (i : ℤ), n < i → ExactAt K i

case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ (∀ (i : ℤ), n < i → ExactAt K i) → K.IsLE n

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → ExactAt K i
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i
⊢ ExactAt K i

Tactic:
rw [not_mem_range_embeddingUpIntLE_iff] at hi

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → ExactAt K i
i : ℤ
hi : n < i
⊢ ExactAt K i

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → ExactAt K i
⊢ K.IsLE n

Tactic:
refine IsSupported.mk (fun i hi ↦ ?_)

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → ExactAt K i
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i
⊢ ExactAt K i

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → ExactAt K i
i : ℤ
hi : n < i
⊢ ExactAt K i

Tactic:
exact h i hi

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
a✝ : K.IsLE n
i : ℤ
hi : n < i
⊢ ExactAt K i

Tactic:
exact K.exactAt_of_isLE n i hi

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsLE n → ∀ (i : ℤ), n < i → ExactAt K i

Tactic:
intro _ i hi

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
a✝ : K.IsLE n
i : ℤ
hi : n < i
⊢ ExactAt K i
-- Mathlib/Geometry/Euclidean/Triangle.lean
theorem angle_add_angle_sub_add_angle_sub_eq_pi {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    angle x y + angle x (x - y) + angle y (y - x) = π

Proof state:
case intro.intro.intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx✝ : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
n : ℤ
hn : angle x y + angle x (x - y) + angle y (y - x) = ↑n * π
h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)
hx : x ≠ 0
r : ℝ
hnlt : ¬π + angle (r • x) (r • x - x) < π + π + π
hr : r < 0
hxr : y = r • x
⊢ π + angle (r • x) (r • x - x) < π + (π + π)

Tactic:
exact add_lt_add_left (lt_of_le_of_lt (angle_le_pi _ _) (lt_add_of_pos_right π Real.pi_pos)) _

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
n : ℤ
hn : angle x y + angle x (x - y) + angle y (y - x) = ↑n * π
h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)
hn0 : 0 ≤ n
h3lt : ↑n < 3
⊢ n < 3

Tactic:
norm_cast at h3lt

Result:
no goals
-- Mathlib/Algebra/Category/FGModuleCat/Basic.lean
theorem coevaluation_evaluation :
    letI V' : FGModuleCat K := FGModuleCatDual K V
    V' ◁ FGModuleCatCoevaluation K V ≫ (α_ V' V V').inv ≫ FGModuleCatEvaluation K V ▷ V' =
      (ρ_ V').hom ≫ (λ_ V').inv

Proof state:
case h
K : Type u
inst✝ : Field K
V : FGModuleCat K
⊢ ModuleCat.Hom.hom
      (FGModuleCatDual K V ◁ FGModuleCatCoevaluation K V ≫
        (α_ (FGModuleCatDual K V) V (FGModuleCatDual K V)).inv ≫ FGModuleCatEvaluation K V ▷ FGModuleCatDual K V) =
    ModuleCat.Hom.hom ((ρ_ (FGModuleCatDual K V)).hom ≫ (λ_ (FGModuleCatDual K V)).inv)

Tactic:
apply contractLeft_assoc_coevaluation K V

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
V : FGModuleCat K
⊢ FGModuleCatDual K V ◁ FGModuleCatCoevaluation K V ≫
      (α_ (FGModuleCatDual K V) V (FGModuleCatDual K V)).inv ≫ FGModuleCatEvaluation K V ▷ FGModuleCatDual K V =
    (ρ_ (FGModuleCatDual K V)).hom ≫ (λ_ (FGModuleCatDual K V)).inv

Tactic:
ext : 1

Result:
case h
K : Type u
inst✝ : Field K
V : FGModuleCat K
⊢ ModuleCat.Hom.hom
      (FGModuleCatDual K V ◁ FGModuleCatCoevaluation K V ≫
        (α_ (FGModuleCatDual K V) V (FGModuleCatDual K V)).inv ≫ FGModuleCatEvaluation K V ▷ FGModuleCatDual K V) =
    ModuleCat.Hom.hom ((ρ_ (FGModuleCatDual K V)).hom ≫ (λ_ (FGModuleCatDual K V)).inv)
-- Mathlib/RingTheory/Kaehler/CotangentComplex.lean
@[simp] lemma H1Cotangent.map_id : map (.id P) = LinearMap.id

Proof state:
case h.e.e
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x✝ : P.H1Cotangent
⊢ (↑((map (Hom.id P)) x✝)).val = (↑(LinearMap.id x✝)).val

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ map (Hom.id P) = LinearMap.id

Tactic:
ext

Result:
case h.e.e
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x✝ : P.H1Cotangent
⊢ (↑((map (Hom.id P)) x✝)).val = (↑(LinearMap.id x✝)).val
-- Mathlib/Data/Matrix/Rank.lean
theorem ker_mulVecLin_conjTranspose_mul_self (A : Matrix m n R) :
    LinearMap.ker (Aᴴ * A).mulVecLin = LinearMap.ker (mulVecLin A)

Proof state:
case h
m : Type u_2
n : Type u_3
R : Type u_5
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : Field R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
A : Matrix m n R
x : n → R
⊢ x ∈ LinearMap.ker (Aᴴ * A).mulVecLin ↔ x ∈ LinearMap.ker A.mulVecLin

Tactic:
simp only [LinearMap.mem_ker, mulVecLin_apply, conjTranspose_mul_self_mulVec_eq_zero]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : Field R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ LinearMap.ker (Aᴴ * A).mulVecLin = LinearMap.ker A.mulVecLin

Tactic:
ext x

Result:
case h
m : Type u_2
n : Type u_3
R : Type u_5
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : Field R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
A : Matrix m n R
x : n → R
⊢ x ∈ LinearMap.ker (Aᴴ * A).mulVecLin ↔ x ∈ LinearMap.ker A.mulVecLin
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_range [DecidableEq α] [Fintype β] (f : β → α) [Fintype (Set.range f)] :
    (Set.range f).toFinset = Finset.univ.image f

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype β
f : β → α
inst✝ : Fintype ↑(range f)
a✝ : α
⊢ a✝ ∈ (range f).toFinset ↔ a✝ ∈ Finset.image f Finset.univ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype β
f : β → α
inst✝ : Fintype ↑(range f)
⊢ (range f).toFinset = Finset.image f Finset.univ

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype β
f : β → α
inst✝ : Fintype ↑(range f)
a✝ : α
⊢ a✝ ∈ (range f).toFinset ↔ a✝ ∈ Finset.image f Finset.univ
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem neighborSet_subgraphOfAdj_of_ne_of_ne {u v w : V} (hvw : G.Adj v w) (hv : u ≠ v)
    (hw : u ≠ w) : (G.subgraphOfAdj hvw).neighborSet u = ∅

Proof state:
case h
V : Type u
G : SimpleGraph V
u v w : V
hvw : G.Adj v w
hv : u ≠ v
hw : u ≠ w
x✝ : V
⊢ x✝ ∈ (G.subgraphOfAdj hvw).neighborSet u ↔ x✝ ∈ ∅

Tactic:
simp [hv.symm, hw.symm]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
hvw : G.Adj v w
hv : u ≠ v
hw : u ≠ w
⊢ (G.subgraphOfAdj hvw).neighborSet u = ∅

Tactic:
ext

Result:
case h
V : Type u
G : SimpleGraph V
u v w : V
hvw : G.Adj v w
hv : u ≠ v
hw : u ≠ w
x✝ : V
⊢ x✝ ∈ (G.subgraphOfAdj hvw).neighborSet u ↔ x✝ ∈ ∅
-- Mathlib/Data/List/Destutter.lean
theorem destutter'_eq_self_iff (a) : l.destutter' R a = a :: l ↔ l.Chain R a :=
  ⟨fun h => by
    suffices Chain' R (a::l) by
      assumption
    rw [← h]
    exact l.destutter'_is_chain' R a, destutter'_of_chain _ _⟩

Proof state:
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
h : destutter' R a l = a :: l
⊢ Chain R a l

Tactic:
suffices Chain' R (a::l) by
  assumption

Result:
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
h : destutter' R a l = a :: l
⊢ Chain' R (a :: l)

Proof state:
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
h : destutter' R a l = a :: l
⊢ Chain' R (destutter' R a l)

Tactic:
exact l.destutter'_is_chain' R a

Result:
no goals

Proof state:
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
h : destutter' R a l = a :: l
this : Chain' R (a :: l)
⊢ Chain R a l

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
h : destutter' R a l = a :: l
⊢ Chain' R (a :: l)

Tactic:
rw [← h]

Result:
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
h : destutter' R a l = a :: l
⊢ Chain' R (destutter' R a l)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_append {x : BitVec n} {y : BitVec m} :
    getMsbD (x ++ y) i = if n ≤ i then getMsbD y (i - n) else getMsbD x i

Proof state:
n m i : Nat
x : BitVec n
y : BitVec m
⊢ i + m - (n + m) = i - n

Tactic:
omega

Result:
no goals

Proof state:
n m i : Nat
x : BitVec n
y : BitVec m
⊢ (x ++ y).getMsbD i = if n ≤ i then y.getMsbD (i - n) else x.getMsbD i

Tactic:
simp only [append_def]

Result:
n m i : Nat
x : BitVec n
y : BitVec m
⊢ (x.shiftLeftZeroExtend m ||| setWidth' ⋯ y).getMsbD i = if n ≤ i then y.getMsbD (i - n) else x.getMsbD i

Proof state:
n m i : Nat
x : BitVec n
y : BitVec m
this : i + m - (n + m) = i - n
⊢ (x.shiftLeftZeroExtend m ||| setWidth' ⋯ y).getMsbD i = if n ≤ i then y.getMsbD (i - n) else x.getMsbD i

Tactic:
by_cases h : n ≤ i

Result:
case pos
n m i : Nat
x : BitVec n
y : BitVec m
this : i + m - (n + m) = i - n
h : n ≤ i
⊢ (x.shiftLeftZeroExtend m ||| setWidth' ⋯ y).getMsbD i = if n ≤ i then y.getMsbD (i - n) else x.getMsbD i

case neg
n m i : Nat
x : BitVec n
y : BitVec m
this : i + m - (n + m) = i - n
h : ¬n ≤ i
⊢ (x.shiftLeftZeroExtend m ||| setWidth' ⋯ y).getMsbD i = if n ≤ i then y.getMsbD (i - n) else x.getMsbD i

Proof state:
case pos
n m i : Nat
x : BitVec n
y : BitVec m
this : i + m - (n + m) = i - n
h : n ≤ i
⊢ (x.shiftLeftZeroExtend m ||| setWidth' ⋯ y).getMsbD i = if n ≤ i then y.getMsbD (i - n) else x.getMsbD i

Tactic:
simp_all

Result:
no goals

Proof state:
case neg
n m i : Nat
x : BitVec n
y : BitVec m
this : i + m - (n + m) = i - n
h : ¬n ≤ i
⊢ (x.shiftLeftZeroExtend m ||| setWidth' ⋯ y).getMsbD i = if n ≤ i then y.getMsbD (i - n) else x.getMsbD i

Tactic:
simp [h]

Result:
no goals

Proof state:
n m i : Nat
x : BitVec n
y : BitVec m
⊢ (x.shiftLeftZeroExtend m ||| setWidth' ⋯ y).getMsbD i = if n ≤ i then y.getMsbD (i - n) else x.getMsbD i

Tactic:
have : i + m - (n + m) = i - n := by omega

Result:
n m i : Nat
x : BitVec n
y : BitVec m
this : i + m - (n + m) = i - n
⊢ (x.shiftLeftZeroExtend m ||| setWidth' ⋯ y).getMsbD i = if n ≤ i then y.getMsbD (i - n) else x.getMsbD i
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getThenInsertIfNew?_fst {k : α} {v : β} : (getThenInsertIfNew? m k v).1 = get? m k

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw₀ α fun x => β
k : α
v : β
⊢ (getThenInsertIfNew? m k v).fst = get? m k

Tactic:
rw [getThenInsertIfNew?_eq_get?ₘ, get?_eq_get?ₘ]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mlieBracketWithin_swap_apply :
    mlieBracketWithin I V W s x = - mlieBracketWithin I W V s x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
⊢ (-mpullback I 𝓘(𝕜, E) (↑(extChartAt I x))
          (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I))
            (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
            (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)))
      x =
    -mlieBracketWithin I W V s x

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
⊢ mlieBracketWithin I V W s x = -mlieBracketWithin I W V s x

Tactic:
rw [mlieBracketWithin, lieBracketWithin_swap, mpullback_neg]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
⊢ (-mpullback I 𝓘(𝕜, E) (↑(extChartAt I x))
          (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I))
            (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
            (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)))
      x =
    -mlieBracketWithin I W V s x
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
/-- A functor between preadditive categories that preserves (zero morphisms and) binary biproducts
    preserves binary products. -/
lemma preservesBinaryProduct_of_preservesBinaryBiproduct {X Y : C}
    [PreservesBinaryBiproduct X Y F] :
    PreservesLimit (pair X Y) F where
  preserves {c} hc := ⟨IsLimit.ofIsoLimit
        ((IsLimit.postcomposeInvEquiv (diagramIsoPair _) _).symm
          (isBinaryBilimitOfPreserves F (binaryBiconeIsBilimitOfLimitConeOfIsLimit hc)).isLimit) <|
      Cones.ext (by dsimp; rfl) fun j => by
        rcases j with ⟨⟨⟩⟩ <;> simp⟩

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cone (pair X Y)
hc : IsLimit c
⊢ F.obj c.pt ≅ F.obj c.pt

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cone (pair X Y)
hc : IsLimit c
⊢ ((Cones.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
        (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)).toCone).pt ≅
    (F.mapCone c).pt

Tactic:
dsimp

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cone (pair X Y)
hc : IsLimit c
⊢ F.obj c.pt ≅ F.obj c.pt

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cone (pair X Y)
hc : IsLimit c
j : Discrete WalkingPair
⊢ ((Cones.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
            (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)).toCone).π.app
      j =
    (id (Iso.refl (F.obj c.pt))).hom ≫ (F.mapCone c).π.app j

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

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem embDomain_add (f : Γ ↪o Γ') (x y : HahnSeries Γ R) :
    embDomain f (x + y) = embDomain f x + embDomain f y

Proof state:
case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
g : Γ'
hg : g ∉ Set.range ⇑f
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g

Tactic:
simp [embDomain_notin_range hg]

Result:
no goals

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
⊢ embDomain f (x + y) = embDomain f x + embDomain f y

Tactic:
ext g

Result:
case coeff.h
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
g : Γ'
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g

Proof state:
case coeff.h
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
g : Γ'
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g

Tactic:
by_cases hg : g ∈ Set.range f

Result:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
g : Γ'
hg : g ∈ Set.range ⇑f
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g

case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
g : Γ'
hg : g ∉ Set.range ⇑f
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g

Proof state:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
g : Γ'
hg : g ∈ Set.range ⇑f
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g

Tactic:
obtain ⟨a, rfl⟩ := hg

Result:
case pos.intro
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
a : Γ
⊢ (embDomain f (x + y)).coeff (f a) = (embDomain f x + embDomain f y).coeff (f a)

Proof state:
case pos.intro
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
a : Γ
⊢ (embDomain f (x + y)).coeff (f a) = (embDomain f x + embDomain f y).coeff (f a)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Smooth/Locus.lean
lemma basicOpen_subset_smoothLocus_iff_smooth [FinitePresentation R A] {f : A} :
    ↑(PrimeSpectrum.basicOpen f) ⊆ smoothLocus R A ↔
      Algebra.Smooth R (Localization.Away f)

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
this : FinitePresentation A (Localization.Away f)
⊢ FormallySmooth R (Localization.Away f) ↔ Smooth R (Localization.Away f)

Tactic:
exact ⟨fun H ↦ ⟨H, .trans _ A _⟩, fun H ↦ H.1⟩

Result:
no goals

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
this : FinitePresentation A (Localization.Away f)
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ smoothLocus R A ↔ Smooth R (Localization.Away f)

Tactic:
rw [basicOpen_subset_smoothLocus_iff]

Result:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
this : FinitePresentation A (Localization.Away f)
⊢ FormallySmooth R (Localization.Away f) ↔ Smooth R (Localization.Away f)

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ smoothLocus R A ↔ Smooth R (Localization.Away f)

Tactic:
have : FinitePresentation A (Localization.Away f) := IsLocalization.Away.finitePresentation f

Result:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
this : FinitePresentation A (Localization.Away f)
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ smoothLocus R A ↔ Smooth R (Localization.Away f)