harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Pi/Basic.lean
theorem elim_one_mulSingle [DecidableEq α] [DecidableEq β] [One γ] (i : β) (c : γ) :
    Sum.elim (1 : α → γ) (Pi.mulSingle i c) = Pi.mulSingle (Sum.inr i) c

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : One γ
i : β
c : γ
⊢ Sum.elim 1 (Pi.mulSingle i c) = Pi.mulSingle (inr i) c

Tactic:
simp only [Pi.mulSingle, Sum.elim_update_right, elim_one_one]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Iic_diff_Ioc : Iic b \ Ioc a b = Iic (a ⊓ b)

Proof state:
α : Type u_2
a b : α
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrderBot α
⊢ ↑(Iic b \ Ioc a b) = ↑(Iic (a ⊓ b))

Tactic:
push_cast

Result:
α : Type u_2
a b : α
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrderBot α
⊢ Set.Iic b \ Set.Ioc a b = Set.Iic (a ⊓ b)

Proof state:
α : Type u_2
a b : α
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrderBot α
⊢ Iic b \ Ioc a b = Iic (a ⊓ b)

Tactic:
rw [← coe_inj]

Result:
α : Type u_2
a b : α
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrderBot α
⊢ ↑(Iic b \ Ioc a b) = ↑(Iic (a ⊓ b))

Proof state:
α : Type u_2
a b : α
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrderBot α
⊢ Set.Iic b \ Set.Ioc a b = Set.Iic (a ⊓ b)

Tactic:
exact Set.Iic_diff_Ioc

Result:
no goals
-- Mathlib/Data/Option/NAry.lean
/-- If `b` is a right identity for a binary operation `f`, then `some b` is a right identity for
`Option.map₂ f`. -/
lemma map₂_right_identity {f : α → β → α} {b : β} (h : ∀ a, f a b = a) (o : Option α) :
    map₂ f o (some b) = o

Proof state:
α : Type u_1
β : Type u_2
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
o : Option α
⊢ map₂ f o (some b) = o

Tactic:
simp [h, map₂]

Result:
no goals
-- Mathlib/Order/Interval/Set/Pi.lean
theorem disjoint_pi_univ_Ioc_update_left_right {x y : ∀ i, α i} {i₀ : ι} {m : α i₀} :
    Disjoint (pi univ fun i ↦ Ioc (x i) (update y i₀ m i))
    (pi univ fun i ↦ Ioc (update x i₀ m i) (y i))

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
z : (i : ι) → α i
h₁ : z ∈ univ.pi fun i => Ioc (x i) (update y i₀ m i)
h₂ : z ∈ univ.pi fun i => Ioc (update x i₀ m i) (y i)
⊢ update y i₀ m i₀ < z i₀

Tactic:
simpa only [Function.update_self] using (h₂ i₀ (mem_univ _)).1

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
z : (i : ι) → α i
h₁ : z ∈ univ.pi fun i => Ioc (x i) (update y i₀ m i)
h₂ : z ∈ univ.pi fun i => Ioc (update x i₀ m i) (y i)
⊢ False

Tactic:
refine (h₁ i₀ (mem_univ _)).2.not_lt ?_

Result:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
z : (i : ι) → α i
h₁ : z ∈ univ.pi fun i => Ioc (x i) (update y i₀ m i)
h₂ : z ∈ univ.pi fun i => Ioc (update x i₀ m i) (y i)
⊢ update y i₀ m i₀ < z i₀

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
⊢ Disjoint (univ.pi fun i => Ioc (x i) (update y i₀ m i)) (univ.pi fun i => Ioc (update x i₀ m i) (y i))

Tactic:
rw [disjoint_left]

Result:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
⊢ ∀ ⦃a : (i : ι) → α i⦄,
    (a ∈ univ.pi fun i => Ioc (x i) (update y i₀ m i)) → a ∉ univ.pi fun i => Ioc (update x i₀ m i) (y i)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
⊢ ∀ ⦃a : (i : ι) → α i⦄,
    (a ∈ univ.pi fun i => Ioc (x i) (update y i₀ m i)) → a ∉ univ.pi fun i => Ioc (update x i₀ m i) (y i)

Tactic:
rintro z h₁ h₂

Result:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
z : (i : ι) → α i
h₁ : z ∈ univ.pi fun i => Ioc (x i) (update y i₀ m i)
h₂ : z ∈ univ.pi fun i => Ioc (update x i₀ m i) (y i)
⊢ False
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem cos_eq_real_cos_iff_eq_or_eq_neg {θ : Angle} {ψ : ℝ} :
    cos θ = Real.cos ψ ↔ θ = ψ ∨ θ = -ψ

Proof state:
θ : Angle
ψ : ℝ
⊢ θ.cos = Real.cos ψ ↔ θ = ↑ψ ∨ θ = -↑ψ

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
ψ x✝ : ℝ
⊢ (↑x✝).cos = Real.cos ψ ↔ ↑x✝ = ↑ψ ∨ ↑x✝ = -↑ψ

Proof state:
case h
ψ x✝ : ℝ
⊢ (↑x✝).cos = Real.cos ψ ↔ ↑x✝ = ↑ψ ∨ ↑x✝ = -↑ψ

Tactic:
exact cos_eq_iff_coe_eq_or_eq_neg

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
lemma IsLocalizedModule.eq_iff_exists [IsLocalizedModule S f] {x₁ x₂} :
    f x₁ = f x₂ ↔ ∃ c : S, c • x₁ = c • x₂ :=
  Iff.intro exists_of_eq fun ⟨c, h⟩ ↦ by
    apply_fun f at h
    simp_rw [f.map_smul_of_tower, Submonoid.smul_def, ← Module.algebraMap_end_apply R R] at h
    exact ((Module.End_isUnit_iff _).mp <| map_units f c).1 h

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x₁ x₂ : M
x✝ : ∃ c, c • x₁ = c • x₂
c : ↥S
h : c • x₁ = c • x₂
⊢ f x₁ = f x₂

Tactic:
apply_fun f at h

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x₁ x₂ : M
x✝ : ∃ c, c • x₁ = c • x₂
c : ↥S
h : f (c • x₁) = f (c • x₂)
⊢ f x₁ = f x₂

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x₁ x₂ : M
x✝ : ∃ c, c • x₁ = c • x₂
c : ↥S
h : ((algebraMap R (Module.End R M')) ↑c) (f x₁) = ((algebraMap R (Module.End R M')) ↑c) (f x₂)
⊢ f x₁ = f x₂

Tactic:
exact ((Module.End_isUnit_iff _).mp <| map_units f c).1 h

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x₁ x₂ : M
x✝ : ∃ c, c • x₁ = c • x₂
c : ↥S
h : f (c • x₁) = f (c • x₂)
⊢ f x₁ = f x₂

Tactic:
simp_rw [f.map_smul_of_tower, Submonoid.smul_def, ← Module.algebraMap_end_apply R R] at h

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x₁ x₂ : M
x✝ : ∃ c, c • x₁ = c • x₂
c : ↥S
h : ((algebraMap R (Module.End R M')) ↑c) (f x₁) = ((algebraMap R (Module.End R M')) ↑c) (f x₂)
⊢ f x₁ = f x₂
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem equalizerSubobject_factors {W : C} (h : W ⟶ X) (w : h ≫ f = h ≫ g) :
    (equalizerSubobject f g).Factors h :=
  ⟨equalizer.lift h w, by simp⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
W : C
h : W ⟶ X
w : h ≫ f = h ≫ g
⊢ equalizer.lift h w ≫ (MonoOver.mk' (equalizer.ι f g)).arrow = h

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_at_one {S : Type*} [Semiring S] (f : R →+* S) : p.eval₂ f 1 = f (p.eval 1)

Proof state:
case h.e'_2.h.e'_6
R : Type u
inst✝¹ : Semiring R
p : R[X]
S : Type u_1
inst✝ : Semiring S
f : R →+* S
⊢ 1 = f 1

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
p : R[X]
S : Type u_1
inst✝ : Semiring S
f : R →+* S
⊢ eval₂ f 1 p = f (eval 1 p)

Tactic:
convert eval₂_at_apply (p := p) f 1

Result:
case h.e'_2.h.e'_6
R : Type u
inst✝¹ : Semiring R
p : R[X]
S : Type u_1
inst✝ : Semiring S
f : R →+* S
⊢ 1 = f 1
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc]
lemma leftRightHomologyComparison_fac [S.HasHomology] :
    S.leftRightHomologyComparison = S.leftHomologyIso.hom ≫ S.rightHomologyIso.inv

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.leftRightHomologyComparison = S.leftHomologyIso.hom ≫ S.rightHomologyIso.inv

Tactic:
simpa only [LeftHomologyData.homologyIso_leftHomologyData, Iso.symm_inv,
  RightHomologyData.homologyIso_rightHomologyData, Iso.symm_hom] using
    leftRightHomologyComparison'_fac S.leftHomologyData S.rightHomologyData

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_ofList [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
    (ofList l).size = l.length

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ (ofList l).size = l.length

Tactic:
simp_to_raw using Raw₀.size_insertMany_empty_list

Result:
no goals
-- Mathlib/Order/Filter/Lift.lean
theorem lift_principal2 {f : Filter α} : f.lift 𝓟 = f :=
  le_antisymm (fun s hs => mem_lift hs (mem_principal_self s))
    (le_iInf fun s => le_iInf fun hs => by simp only [hs, le_principal_iff])

Proof state:
α : Type u_1
f : Filter α
s : Set α
hs : s ∈ f
⊢ f ≤ 𝓟 s

Tactic:
simp only [hs, le_principal_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem det_of_upperTriangular [LinearOrder m] (h : M.BlockTriangular id) :
    M.det = ∏ i : m, M i i

Proof state:
m : Type u_3
R : Type v
M : Matrix m m R
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : LinearOrder m
h : M.BlockTriangular id
⊢ M.det = ∏ i : m, M i i

Tactic:
haveI : DecidableEq R := Classical.decEq _

Result:
m : Type u_3
R : Type v
M : Matrix m m R
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : LinearOrder m
h : M.BlockTriangular id
this : DecidableEq R
⊢ M.det = ∏ i : m, M i i

Proof state:
m : Type u_3
R : Type v
M : Matrix m m R
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : LinearOrder m
h : M.BlockTriangular id
this : DecidableEq R
⊢ M.det = ∏ i : m, M i i

Tactic:
simp_rw [h.det, image_id, det_toSquareBlock_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mul_div_mul_right {m : Nat} (n k : Nat) (H : 0 < m) :
    n * m / (k * m) = n / k

Proof state:
m n k : Nat
H : 0 < m
⊢ n * m / (k * m) = n / k

Tactic:
rw [Nat.mul_comm, Nat.mul_comm k, Nat.mul_div_mul_left _ _ H]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsCycles.existsUnique_ne_adj (h : G.IsCycles) (hadj : G.Adj v w) :
    ∃! w', w ≠ w' ∧ G.Adj v w'

Proof state:
case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
⊢ (fun w' => w ≠ w' ∧ G.Adj v w') w' ∧ ∀ (y : V), (fun w' => w ≠ w' ∧ G.Adj v w') y → y = w'

Tactic:
refine ⟨⟨hww, hww'⟩, ?_⟩

Result:
case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
⊢ ∀ (y : V), (fun w' => w ≠ w' ∧ G.Adj v w') y → y = w'

Proof state:
case h.intro.intro
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
w' : V
hww : w ≠ w'
y : V
hwy : w ≠ y
x y' : V
hxy' : x ≠ y' ∧ G.neighborSet v = {x, y'}
hadj : w ∈ G.neighborSet v
hww' : w' ∈ G.neighborSet v
hwy' : y ∈ G.neighborSet v
⊢ y = w'

Tactic:
aesop

Result:
no goals

Proof state:
case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
⊢ ∀ (y : V), (fun w' => w ≠ w' ∧ G.Adj v w') y → y = w'

Tactic:
intro y ⟨hwy, hwy'⟩

Result:
case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
y : V
hwy : w ≠ y
hwy' : G.Adj v y
⊢ y = w'

Proof state:
case h.intro.intro
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
y : V
hwy : w ≠ y
hwy' : G.Adj v y
x y' : V
hxy' : x ≠ y' ∧ G.neighborSet v = {x, y'}
⊢ y = w'

Tactic:
simp_rw [← SimpleGraph.mem_neighborSet] at *

Result:
case h.intro.intro
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
w' : V
hww : w ≠ w'
y : V
hwy : w ≠ y
x y' : V
hxy' : x ≠ y' ∧ G.neighborSet v = {x, y'}
hadj : w ∈ G.neighborSet v
hww' : w' ∈ G.neighborSet v
hwy' : y ∈ G.neighborSet v
⊢ y = w'

Proof state:
case intro.intro
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
⊢ ∃! w', w ≠ w' ∧ G.Adj v w'

Tactic:
use w'

Result:
case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
⊢ (fun w' => w ≠ w' ∧ G.Adj v w') w' ∧ ∀ (y : V), (fun w' => w ≠ w' ∧ G.Adj v w') y → y = w'

Proof state:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
⊢ ∃! w', w ≠ w' ∧ G.Adj v w'

Tactic:
obtain ⟨w', ⟨hww, hww'⟩⟩ := h.other_adj_of_adj hadj

Result:
case intro.intro
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
⊢ ∃! w', w ≠ w' ∧ G.Adj v w'

Proof state:
case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
y : V
hwy : w ≠ y
hwy' : G.Adj v y
⊢ y = w'

Tactic:
obtain ⟨x, y', hxy'⟩ := Set.ncard_eq_two.mp (h ⟨w, hadj⟩)

Result:
case h.intro.intro
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
y : V
hwy : w ≠ y
hwy' : G.Adj v y
x y' : V
hxy' : x ≠ y' ∧ G.neighborSet v = {x, y'}
⊢ y = w'
-- Mathlib/Geometry/Euclidean/Inversion/Basic.lean
theorem dist_inversion_center (c x : P) (R : ℝ) : dist (inversion c R x) c = R ^ 2 / dist x c

Proof state:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
hx : x ≠ c
⊢ dist (inversion c R x) c = R ^ 2 / dist x c

Tactic:
have : dist x c ≠ 0 := dist_ne_zero.2 hx

Result:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
hx : x ≠ c
this : dist x c ≠ 0
⊢ dist (inversion c R x) c = R ^ 2 / dist x c

Proof state:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
hx : x ≠ c
this : dist x c ≠ 0
⊢ dist (inversion c R x) c = R ^ 2 / dist x c

Tactic:
simp (disch := field_simp_discharge) only [inversion, sq, mul_div_assoc', div_mul_eq_mul_div,
  div_div, dist_vadd_left, norm_smul, norm_div, norm_mul, Real.norm_eq_abs, abs_mul_abs_self,
  abs_dist, ← dist_eq_norm_vsub, mul_assoc, eq_div_iff, div_eq_iff]

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
c x : P
R : ℝ
⊢ dist (inversion c R x) c = R ^ 2 / dist x c

Tactic:
rcases eq_or_ne x c with (rfl | hx)

Result:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x : P
R : ℝ
⊢ dist (inversion x R x) x = R ^ 2 / dist x x

case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
hx : x ≠ c
⊢ dist (inversion c R x) c = R ^ 2 / dist x c

Proof state:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x : P
R : ℝ
⊢ dist (inversion x R x) x = R ^ 2 / dist x x

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
theorem r_one_zpow (k : ℤ) : (r 1 : DihedralGroup n) ^ k = r k

Proof state:
n : ℕ
k : ℤ
⊢ r 1 ^ k = r ↑k

Tactic:
simp only [r_zpow, one_mul]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem circumsphere_eq_of_cospherical_subset {s : AffineSubspace ℝ P} {ps : Set P} (h : ps ⊆ s)
    [Nonempty s] {n : ℕ} [FiniteDimensional ℝ s.direction] (hd : finrank ℝ s.direction = n)
    (hc : Cospherical ps) {sx₁ sx₂ : Simplex ℝ P n} (hsx₁ : Set.range sx₁.points ⊆ ps)
    (hsx₂ : Set.range sx₂.points ⊆ ps) : sx₁.circumsphere = sx₂.circumsphere

Proof state:
case intro
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : Sphere P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = r
⊢ sx₁.circumsphere = sx₂.circumsphere

Tactic:
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]

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
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
⊢ sx₁.circumsphere = sx₂.circumsphere

Tactic:
rcases exists_circumsphere_eq_of_cospherical_subset h hd hc with ⟨r, hr⟩

Result:
case intro
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : Sphere P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = r
⊢ sx₁.circumsphere = sx₂.circumsphere
-- Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean
theorem directSum_lof_tmul_lof (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) :
    TensorProduct.directSum R S M₁ M₂ (DirectSum.lof S ι₁ M₁ i₁ m₁ ⊗ₜ DirectSum.lof R ι₂ M₂ i₂ m₂) =
      DirectSum.lof S (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂) (m₁ ⊗ₜ m₂)

Proof state:
R : Type u
inst✝¹⁰ : CommSemiring R
S : Type u_1
inst✝⁹ : Semiring S
inst✝⁸ : Algebra R S
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁷ : DecidableEq ι₁
inst✝⁶ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₂ : ι₂ → Type w₂
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
i₁ : ι₁
m₁ : M₁ i₁
i₂ : ι₂
m₂ : M₂ i₂
⊢ (TensorProduct.directSum R S M₁ M₂) ((lof S ι₁ M₁ i₁) m₁ ⊗ₜ[R] (lof R ι₂ M₂ i₂) m₂) =
    (lof S (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)

Tactic:
simp [TensorProduct.directSum]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem if_false_right [h : Decidable p] :
    ite p q False ↔ p ∧ q

Proof state:
case isTrue
p q : Prop
g : p
⊢ (if p then q else False) ↔ p ∧ q

Tactic:
simp [g]

Result:
no goals

Proof state:
case isTrue
p q : Prop
h✝ : p
⊢ (if p then q else False) ↔ p ∧ q

Tactic:
rename_i g

Result:
case isTrue
p q : Prop
g : p
⊢ (if p then q else False) ↔ p ∧ q

Proof state:
p q : Prop
h : Decidable p
⊢ (if p then q else False) ↔ p ∧ q

Tactic:
cases h <;> (rename_i g; simp [g])

Result:
no goals
-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.quotKerTotalEquiv_symm_comp_D :
    (KaehlerDifferential.quotKerTotalEquiv R S).symm.toLinearMap.compDer
        (KaehlerDifferential.D R S) =
      KaehlerDifferential.derivationQuotKerTotal R S

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (↑(quotKerTotalEquiv R S).symm).compDer (D R S) = derivationQuotKerTotal R S

Tactic:
convert (KaehlerDifferential.derivationQuotKerTotal R S).liftKaehlerDifferential_comp

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma toReal_ne_zero_iff {x : EReal} : x.toReal ≠ 0 ↔ x ≠ 0 ∧ x ≠ ⊤ ∧ x ≠ ⊥

Proof state:
x : EReal
⊢ x.toReal ≠ 0 ↔ x ≠ 0 ∧ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
simp only [ne_eq, toReal_eq_zero_iff, not_or]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #v[] (by simp) = #v[] := rfl

Proof state:
α : Type ?u.8364
β : Type ?u.8363
P : α → Prop
f : (a : α) → P a → β
⊢ ∀ (a : α), a ∈ { toArray := #[], size_toArray := ⋯ } → P a

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Embedding/Basic.lean
lemma setValue_eq_of_ne {α β} {f : α ↪ β} {a : α} {b : β} {c : α} [∀ a', Decidable (a' = a)]
    [∀ a', Decidable (f a' = b)] (hc : c ≠ a) (hb : f c ≠ b) : setValue f a b c = f c

Proof state:
α : Sort u_1
β : Sort u_2
f : α ↪ β
a : α
b : β
c : α
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (f a' = b)
hc : c ≠ a
hb : f c ≠ b
⊢ (f.setValue a b) c = f c

Tactic:
simp [setValue, hc, hb]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem kahler_rotation_right (x y : V) (θ : Real.Angle) :
    o.kahler x (o.rotation θ y) = θ.toCircle * o.kahler x y

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
⊢ ↑θ.cos * (o.kahler x) y + ↑θ.sin * (I * (o.kahler x) y) = (↑θ.cos + ↑θ.sin * I) * (o.kahler x) y

Tactic:
ring

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
⊢ (o.kahler x) ((o.rotation θ) y) = ↑θ.toCircle * (o.kahler x) y

Tactic:
simp only [o.rotation_apply, map_add, LinearMap.map_smulₛₗ, RingHom.id_apply, real_smul,
  kahler_rightAngleRotation_right, Real.Angle.coe_toCircle]

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
⊢ ↑θ.cos * (o.kahler x) y + ↑θ.sin * (I * (o.kahler x) y) = (↑θ.cos + ↑θ.sin * I) * (o.kahler x) y
-- Mathlib/Data/Finset/Sigma.lean
theorem not_mem_sigmaLift_of_ne_right (f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) {a : Sigma α}
    (b : Sigma β) {x : Sigma γ} (h : b.1 ≠ x.1) : x ∉ sigmaLift f a b

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
h : b.fst ≠ x.fst
⊢ x ∉ sigmaLift f a b

Tactic:
rw [mem_sigmaLift]

Result:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
h : b.fst ≠ x.fst
⊢ ¬∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
h : b.fst ≠ x.fst
⊢ ¬∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)

Tactic:
exact fun H => h H.snd.fst

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem _root_.MeasurableSet.exists_isCompact_isClosed_lt_add
    [InnerRegularCompactLTTop μ] [R1Space α] [BorelSpace α]
    ⦃A : Set α⦄ (hA : MeasurableSet A) (h'A : μ A ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ K, K ⊆ A ∧ IsCompact K ∧ IsClosed K ∧ μ A < μ K + ε :=
  let ⟨K, hKA, hK, hμK⟩ := hA.exists_isCompact_lt_add h'A hε
  ⟨closure K, hK.closure_subset_measurableSet hA hKA, hK.closure, isClosed_closure,
    by rwa [hK.measure_closure]⟩

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : R1Space α
inst✝ : BorelSpace α
A : Set α
hA : MeasurableSet A
h'A : μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
K : Set α
hKA : K ⊆ A
hK : IsCompact K
hμK : μ A < μ K + ε
⊢ μ A < μ (closure K) + ε

Tactic:
rwa [hK.measure_closure]

Result:
no goals