harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Heyting/Basic.lean
theorem Disjoint.sup_sdiff_cancel_right (h : Disjoint a b) : (a ⊔ b) \ b = a

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
⊢ (a ⊔ b) \ b = a

Tactic:
rw [sup_sdiff, sdiff_self, sup_bot_eq, h.sdiff_eq_left]

Result:
no goals
-- Mathlib/Topology/UniformSpace/HeineCantor.lean
theorem ContinuousOn.tendstoUniformly [LocallyCompactSpace α] [CompactSpace β] [UniformSpace γ]
    {f : α → β → γ} {x : α} {U : Set α} (hxU : U ∈ 𝓝 x) (h : ContinuousOn (↿f) (U ×ˢ univ)) :
    TendstoUniformly f (f x) (𝓝 x)

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : CompactSpace β
inst✝ : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (U ×ˢ univ)
K : Set α
hxK : K ∈ 𝓝 x
hKU : K ⊆ U
hK : IsCompact K
⊢ TendstoUniformly f (f x) (𝓝 x)

Tactic:
have : UniformContinuousOn (↿f) (K ×ˢ univ) :=
  IsCompact.uniformContinuousOn_of_continuous (hK.prod isCompact_univ)
    (h.mono <| prod_mono hKU Subset.rfl)

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : CompactSpace β
inst✝ : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (U ×ˢ univ)
K : Set α
hxK : K ∈ 𝓝 x
hKU : K ⊆ U
hK : IsCompact K
this : UniformContinuousOn (↿f) (K ×ˢ univ)
⊢ TendstoUniformly f (f x) (𝓝 x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : CompactSpace β
inst✝ : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (U ×ˢ univ)
⊢ TendstoUniformly f (f x) (𝓝 x)

Tactic:
rcases LocallyCompactSpace.local_compact_nhds _ _ hxU with ⟨K, hxK, hKU, hK⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : CompactSpace β
inst✝ : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (U ×ˢ univ)
K : Set α
hxK : K ∈ 𝓝 x
hKU : K ⊆ U
hK : IsCompact K
⊢ TendstoUniformly f (f x) (𝓝 x)

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : CompactSpace β
inst✝ : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (U ×ˢ univ)
K : Set α
hxK : K ∈ 𝓝 x
hKU : K ⊆ U
hK : IsCompact K
this : UniformContinuousOn (↿f) (K ×ˢ univ)
⊢ TendstoUniformly f (f x) (𝓝 x)

Tactic:
exact this.tendstoUniformly hxK

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem toJordanDecomposition_smul (s : SignedMeasure α) (r : ℝ≥0) :
    (r • s).toJordanDecomposition = r • s.toJordanDecomposition

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition

Tactic:
apply toSignedMeasure_injective

Result:
case a
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ (r • s).toJordanDecomposition.toSignedMeasure = (r • s.toJordanDecomposition).toSignedMeasure

Proof state:
case a
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ (r • s).toJordanDecomposition.toSignedMeasure = (r • s.toJordanDecomposition).toSignedMeasure

Tactic:
simp [toSignedMeasure_smul]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem tan_eq_inv_of_two_zsmul_add_two_zsmul_eq_pi {θ ψ : Angle}
    (h : (2 : ℤ) • θ + (2 : ℤ) • ψ = π) : tan ψ = (tan θ)⁻¹

Proof state:
θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ ψ.tan = θ.tan⁻¹

Tactic:
exact tan_eq_inv_of_two_nsmul_add_two_nsmul_eq_pi h

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem norm_of_mem_sphere {x : Fin n → ℕ} (hx : x ∈ sphere n d k) :
    ‖(WithLp.equiv 2 _).symm ((↑) ∘ x : Fin n → ℝ)‖ = √↑k

Proof state:
n d k : ℕ
x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ √(∑ i : Fin n, |↑(x i)| ^ 2) = √↑k

Tactic:
simp_rw [abs_cast, ← cast_pow, ← cast_sum, (mem_filter.1 hx).2]

Result:
no goals

Proof state:
n d k : ℕ
x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ √(∑ i : Fin n, ‖(WithLp.equiv 2 (Fin n → ℝ)).symm (Nat.cast ∘ x) i‖ ^ 2) = √↑k

Tactic:
dsimp

Result:
n d k : ℕ
x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ √(∑ i : Fin n, |↑(x i)| ^ 2) = √↑k

Proof state:
n d k : ℕ
x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ ‖(WithLp.equiv 2 (Fin n → ℝ)).symm (Nat.cast ∘ x)‖ = √↑k

Tactic:
rw [EuclideanSpace.norm_eq]

Result:
n d k : ℕ
x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ √(∑ i : Fin n, ‖(WithLp.equiv 2 (Fin n → ℝ)).symm (Nat.cast ∘ x) i‖ ^ 2) = √↑k
-- Mathlib/RingTheory/RootsOfUnity/Basic.lean
theorem rootsOfUnity.coe_pow [CommMonoid R] (ζ : rootsOfUnity k R) (m : ℕ) :
    (((ζ ^ m :) : Rˣ) : R) = ((ζ : Rˣ) : R) ^ m

Proof state:
R : Type u_4
k : ℕ
inst✝ : CommMonoid R
ζ : ↥(rootsOfUnity k R)
m : ℕ
⊢ ↑↑(ζ ^ m) = ↑↑ζ ^ m

Tactic:
rw [Subgroup.coe_pow, Units.val_pow_eq_pow_val]

Result:
no goals
-- Mathlib/RingTheory/Localization/NumDen.lean
theorem num_mul_den_eq_num_iff_eq' {x y : K} :
    y * algebraMap A K (den A x) = algebraMap A K (num A x) ↔ x = y :=
  ⟨fun h ↦ by simpa only [eq_comm, mk'_num_den] using eq_mk'_iff_mul_eq.mpr h, fun h ↦
    eq_mk'_iff_mul_eq.mp (by rw [h, mk'_num_den])⟩

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : x = y
⊢ y = mk' K (num A x) (den A x)

Tactic:
rw [h, mk'_num_den]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : y * (algebraMap A K) ↑(den A x) = (algebraMap A K) (num A x)
⊢ x = y

Tactic:
simpa only [eq_comm, mk'_num_den] using eq_mk'_iff_mul_eq.mpr h

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem affineSegment_eq_segment (x y : V) : affineSegment R x y = segment R x y

Proof state:
R : Type u_1
V : Type u_2
inst✝² : OrderedRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ affineSegment R x y = segment R x y

Tactic:
rw [segment_eq_image_lineMap, affineSegment]

Result:
no goals
-- Mathlib/Order/CompleteLatticeIntervals.lean
theorem subset_sInf_of_within [Inhabited s] {t : Set s}
    (h' : t.Nonempty) (h'' : BddBelow t) (h : sInf ((↑) '' t : Set α) ∈ s) :
    sInf ((↑) '' t : Set α) = (@sInf s _ t : α)

Proof state:
α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : InfSet α
inst✝ : Inhabited ↑s
t : Set ↑s
h' : t.Nonempty
h'' : BddBelow t
h : sInf (Subtype.val '' t) ∈ s
⊢ sInf (Subtype.val '' t) = ↑(sInf t)

Tactic:
simp [dif_pos, h, h', h'']

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem map_inl (f : M →ₗ[R'] N) (r : R') : map f (inl r) = inl r

Proof state:
R' : Type u
M : Type v
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R' M
inst✝⁵ : Module R'ᵐᵒᵖ M
inst✝⁴ : IsCentralScalar R' M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R' N
inst✝¹ : Module R'ᵐᵒᵖ N
inst✝ : IsCentralScalar R' N
f : M →ₗ[R'] N
r : R'
⊢ (map f) (inl r) = inl r

Tactic:
rw [map, liftEquivOfComm_apply, lift_apply_inl, Algebra.ofId_apply, algebraMap_eq_inl]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem prod_set' (L : List G) (n : ℕ) (a : G) :
    (L.set n a).prod = L.prod * if hn : n < L.length then L[n]⁻¹ * a else 1

Proof state:
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
⊢ (L.set n a).prod = L.prod * if hn : n < L.length then L[n]⁻¹ * a else 1

Tactic:
refine (prod_set L n a).trans ?_

Result:
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
⊢ ((take n L).prod * if n < L.length then a else 1) * (drop (n + 1) L).prod =
    L.prod * if hn : n < L.length then L[n]⁻¹ * a else 1

Proof state:
case neg
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : ¬n < L.length
⊢ (take n L).prod * 1 * (drop (n + 1) L).prod = L.prod * 1

Tactic:
simp only [take_of_length_le (le_of_not_lt hn), prod_nil, mul_one,
  drop_eq_nil_of_le ((le_of_not_lt hn).trans n.le_succ)]

Result:
no goals

Proof state:
case pos
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : n < L.length
⊢ (take n L).prod * a * (drop (n + 1) L).prod = L.prod * (L[n]⁻¹ * a)

Tactic:
rw [mul_comm _ a, mul_assoc a, prod_drop_succ L n hn, mul_comm _ (drop n L).prod, ←
  mul_assoc (take n L).prod, prod_take_mul_prod_drop, mul_comm a, mul_assoc]

Result:
no goals

Proof state:
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
⊢ ((take n L).prod * if n < L.length then a else 1) * (drop (n + 1) L).prod =
    L.prod * if hn : n < L.length then L[n]⁻¹ * a else 1

Tactic:
split_ifs with hn

Result:
case pos
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : n < L.length
⊢ (take n L).prod * a * (drop (n + 1) L).prod = L.prod * (L[n]⁻¹ * a)

case neg
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : ¬n < L.length
⊢ (take n L).prod * 1 * (drop (n + 1) L).prod = L.prod * 1
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem toLinearPMap_apply_aux {g : Submodule R (E × F)}
    (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0)
    (x : g.map (LinearMap.fst R E F)) :
    g.toLinearPMap x = valFromGraph hg x.2

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ (g.toLinearPMapAux ?hc) x = valFromGraph hg ⋯

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ ↑g.toLinearPMap x = valFromGraph hg ⋯

Tactic:
change (if hg : _ then g.toLinearPMapAux hg else 0) x = _

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ (if hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0 then g.toLinearPMapAux hg else 0) x = valFromGraph hg ⋯

Proof state:
case hc
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ ∀ x ∈ g, x.1 = 0 → x.2 = 0

Tactic:
exact hg

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ (if hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0 then g.toLinearPMapAux hg else 0) x = valFromGraph hg ⋯

Tactic:
rw [dif_pos]

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ (g.toLinearPMapAux ?hc) x = valFromGraph hg ⋯

case hc
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ ∀ x ∈ g, x.1 = 0 → x.2 = 0
-- Mathlib/Topology/LocallyConstant/Basic.lean
theorem locallyConstant_eq_of_fiber_zero_eq {X : Type*} [TopologicalSpace X]
    (f g : LocallyConstant X (Fin 2)) (h : f ⁻¹' ({0} : Set (Fin 2)) = g ⁻¹' {0}) : f = g

Proof state:
X : Type u_5
inst✝ : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h : ⇑f ⁻¹' {0} = ⇑g ⁻¹' {0}
⊢ f = g

Tactic:
simp only [Set.ext_iff, mem_singleton_iff, mem_preimage] at h

Result:
X : Type u_5
inst✝ : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h : ∀ (x : X), f x = 0 ↔ g x = 0
⊢ f = g

Proof state:
X : Type u_5
inst✝ : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h : ∀ (x : X), f x = 0 ↔ g x = 0
⊢ f = g

Tactic:
ext1 x

Result:
case h
X : Type u_5
inst✝ : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h : ∀ (x : X), f x = 0 ↔ g x = 0
x : X
⊢ f x = g x

Proof state:
case h
X : Type u_5
inst✝ : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h : ∀ (x : X), f x = 0 ↔ g x = 0
x : X
⊢ f x = g x

Tactic:
exact Fin.fin_two_eq_of_eq_zero_iff (h x)

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_eq_self {a : α} : fract a = a ↔ 0 ≤ a ∧ a < 1 :=
  fract_eq_iff.trans <| and_assoc.symm.trans <| and_iff_left ⟨0, by simp⟩

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ a - a = ↑0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fintype/Pi.lean
theorem piFinset_eq_empty : piFinset s = ∅ ↔ ∃ i, s i = ∅

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
γ : α → Type u_3
s : (a : α) → Finset (γ a)
⊢ piFinset s = ∅ ↔ ∃ i, s i = ∅

Tactic:
simp [piFinset]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maximal.lean
theorem IsMaximal.coprime_of_ne {M M' : Ideal α} (hM : M.IsMaximal) (hM' : M'.IsMaximal)
    (hne : M ≠ M') : M ⊔ M' = ⊤

Proof state:
α : Type u
inst✝ : Semiring α
M M' : Ideal α
hM : M.IsMaximal
hM' : M'.IsMaximal
hne : M ≠ M'
⊢ M ⊔ M' = ⊤

Tactic:
contrapose! hne with h

Result:
α : Type u
inst✝ : Semiring α
M M' : Ideal α
hM : M.IsMaximal
hM' : M'.IsMaximal
h : M ⊔ M' ≠ ⊤
⊢ M = M'

Proof state:
α : Type u
inst✝ : Semiring α
M M' : Ideal α
hM : M.IsMaximal
hM' : M'.IsMaximal
h : M ⊔ M' ≠ ⊤
⊢ M = M'

Tactic:
exact hM.eq_of_le hM'.ne_top (le_sup_left.trans_eq (hM'.eq_of_le h le_sup_right).symm)

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
theorem isProbabilityMeasure {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt : μ s ≠ ∞)
    (hu : IsUniform X s ℙ μ) : IsProbabilityMeasure ℙ :=
  ⟨by
    have : X ⁻¹' Set.univ = Set.univ := Set.preimage_univ
    rw [← this, hu.measure_preimage hns hnt MeasurableSet.univ, Set.inter_univ,
      ENNReal.div_self hns hnt]⟩

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ⊤
hu : IsUniform X s ℙ μ
⊢ ℙ Set.univ = 1

Tactic:
have : X ⁻¹' Set.univ = Set.univ := Set.preimage_univ

Result:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ⊤
hu : IsUniform X s ℙ μ
this : X ⁻¹' Set.univ = Set.univ
⊢ ℙ Set.univ = 1

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ⊤
hu : IsUniform X s ℙ μ
this : X ⁻¹' Set.univ = Set.univ
⊢ ℙ Set.univ = 1

Tactic:
rw [← this, hu.measure_preimage hns hnt MeasurableSet.univ, Set.inter_univ,
  ENNReal.div_self hns hnt]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem sin_oangle_right_mul_dist_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P}
    (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) : Real.Angle.sin (∡ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ (∡ p₂ p₃ p₁).sin * dist p₁ p₃ = dist p₁ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
  sin_angle_mul_dist_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)]

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₂ p₃ p₁).sign = 1

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

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₂ p₃ p₁).sin * dist p₁ p₃ = dist p₁ p₂

Tactic:
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ (∡ p₂ p₃ p₁).sin * dist p₁ p₃ = dist p₁ p₂
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem dest_corec (g : α → P α) (x : α) : M.dest (M.corec g x) = P.map (M.corec g) (g x)

Proof state:
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
x : α
⊢ (M.corec g x).dest = P.map (M.corec g) (g x)

Tactic:
rw [corec_def, dest_mk]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mul_add_mod_mul {w x : Ordinal} (hw : w < x) (y z : Ordinal) :
    (x * y + w) % (x * z) = x * (y % z) + w

Proof state:
case h
w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ x * z * (y / z) + (x * (y % z) + w) = x * y + w

Tactic:
rw [← add_assoc, mul_assoc, ← mul_add, div_add_mod]

Result:
no goals

Proof state:
w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ (x * y + w) % (x * z) = x * (y % z) + w

Tactic:
rw [mod_def, mul_add_div_mul hw]

Result:
w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ x * y + w - x * z * (y / z) = x * (y % z) + w

Proof state:
w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ x * y + w - x * z * (y / z) = x * (y % z) + w

Tactic:
apply sub_eq_of_add_eq

Result:
case h
w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ x * z * (y / z) + (x * (y % z) + w) = x * y + w
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem pow_card_pow {n p : ℕ} [Fact p.Prime] (x : ZMod p) : x ^ p ^ n = x

Proof state:
n p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
⊢ x ^ p ^ n = x

Tactic:
induction n with
| zero => simp
| succ n ih => simp [pow_succ, pow_mul, ih, pow_card]

Result:
no goals

Proof state:
case zero
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
⊢ x ^ p ^ 0 = x

Tactic:
simp

Result:
no goals

Proof state:
case succ
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
n : ℕ
ih : x ^ p ^ n = x
⊢ x ^ p ^ (n + 1) = x

Tactic:
simp [pow_succ, pow_mul, ih, pow_card]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem and_congr (w : Nat) (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
    lhs' &&& rhs' = lhs &&& rhs

Proof state:
w : Nat
lhs rhs lhs' rhs' : BitVec w
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs' &&& rhs' = lhs &&& rhs

Tactic:
simp[*]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean
theorem braiding_naturality_right (X : ModuleCat R) {Y Z : ModuleCat R} (f : Y ⟶ Z) :
    X ◁ f ≫ (braiding X Z).hom = (braiding X Y).hom ≫ f ▷ X

Proof state:
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
f : Y ⟶ Z
⊢ (𝟙 X ⊗ f) ≫ (X.braiding Z).hom = (X.braiding Y).hom ≫ f ▷ X

Tactic:
apply braiding_naturality

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
f : Y ⟶ Z
⊢ X ◁ f ≫ (X.braiding Z).hom = (X.braiding Y).hom ≫ f ▷ X

Tactic:
simp_rw [← id_tensorHom]

Result:
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
f : Y ⟶ Z
⊢ (𝟙 X ⊗ f) ≫ (X.braiding Z).hom = (X.braiding Y).hom ≫ f ▷ X
-- Mathlib/Data/Set/Lattice.lean
theorem iInter₂_union (s : ∀ i, κ i → Set α) (t : Set α) :
    (⋂ (i) (j), s i j) ∪ t = ⋂ (i) (j), s i j ∪ t

Proof state:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋂ i, ⋂ j, s i j) ∪ t = ⋂ i, ⋂ j, s i j ∪ t

Tactic:
simp_rw [iInter_union]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_modify (h : m.1.WF) {k k' : α} {f : β k → β k}
    (hc : (m.modify k f).contains k') :
    (m.modify k f).get k' hc =
      if heq : k == k' then
        haveI h' : m.contains k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k k' : α
f : β k → β k
hc : (m.modify k f).contains k' = true
heq : (k == k') = true
⊢ m.contains k = true

Tactic:
rwa [contains_modify _ h, ← eq_of_beq heq] at hc

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k k' : α
f : β k → β k
hc : (m.modify k f).contains k' = true
heq : ¬(k == k') = true
⊢ m.contains k' = true

Tactic:
rwa [contains_modify _ h] at hc

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k k' : α
f : β k → β k
hc : (m.modify k f).contains k' = true
⊢ (m.modify k f).get k' hc = if heq : (k == k') = true then cast ⋯ (f (m.get k ⋯)) else m.get k' ⋯

Tactic:
simp_to_model [modify] using List.getValueCast_modifyKey

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem get?_set (a : Array α) (i : Nat) (h : i < a.size) (j : Nat) (v : α) :
    (a.set i v)[j]? = if i = j then some v else a[j]?

Proof state:
α : Type u_1
a : Array α
i : Nat
h : i < a.size
v : α
⊢ (a.set i v h)[i]? = if i = i then some v else a[i]?

Tactic:
simp [*]

Result:
no goals

Proof state:
α : Type u_1
a : Array α
i : Nat
h✝ : i < a.size
j : Nat
v : α
h : i = j
⊢ (a.set i v h✝)[j]? = if i = j then some v else a[j]?

Tactic:
subst j

Result:
α : Type u_1
a : Array α
i : Nat
h : i < a.size
v : α
⊢ (a.set i v h)[i]? = if i = i then some v else a[i]?

Proof state:
α : Type u_1
a : Array α
i : Nat
h : i < a.size
j : Nat
v : α
⊢ (a.set i v h)[j]? = if i = j then some v else a[j]?

Tactic:
if h : i = j then subst j; simp [*] else simp [*]

Result:
no goals

Proof state:
α : Type u_1
a : Array α
i : Nat
h✝ : i < a.size
j : Nat
v : α
h : ¬i = j
⊢ (a.set i v h✝)[j]? = if i = j then some v else a[j]?

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem isPath_iff_eq_nil {u : V} (p : G.Walk u u) : p.IsPath ↔ p = nil

Proof state:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.IsPath ↔ p = nil

Tactic:
cases p <;> simp [IsPath.nil]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lcm.lean
theorem dvd_lcm_left (m n : Nat) : m ∣ lcm m n :=
  ⟨n / gcd m n, by rw [← Nat.mul_div_assoc m (Nat.gcd_dvd_right m n)]; rfl⟩

Proof state:
m n : Nat
⊢ m.lcm n = m * n / m.gcd n

Tactic:
rfl

Result:
no goals

Proof state:
m n : Nat
⊢ m.lcm n = m * (n / m.gcd n)

Tactic:
rw [← Nat.mul_div_assoc m (Nat.gcd_dvd_right m n)]

Result:
m n : Nat
⊢ m.lcm n = m * n / m.gcd n
-- Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
theorem prod_isUnit : ∀ {L : List M}, (∀ m ∈ L, IsUnit m) → IsUnit L.prod
  | [], _ => by simp
  | h :: t, u => by
    simp only [List.prod_cons]
    exact IsUnit.mul (u h (mem_cons_self h t)) (prod_isUnit fun m mt => u m (mem_cons_of_mem h mt))

Proof state:
M : Type u_4
inst✝ : Monoid M
h : M
t : List M
u : ∀ m ∈ h :: t, IsUnit m
⊢ IsUnit (h * t.prod)

Tactic:
exact IsUnit.mul (u h (mem_cons_self h t)) (prod_isUnit fun m mt => u m (mem_cons_of_mem h mt))

Result:
no goals

Proof state:
M : Type u_4
inst✝ : Monoid M
h : M
t : List M
u : ∀ m ∈ h :: t, IsUnit m
⊢ IsUnit (h :: t).prod

Tactic:
simp only [List.prod_cons]

Result:
M : Type u_4
inst✝ : Monoid M
h : M
t : List M
u : ∀ m ∈ h :: t, IsUnit m
⊢ IsUnit (h * t.prod)

Proof state:
M : Type u_4
inst✝ : Monoid M
x✝ : ∀ m ∈ [], IsUnit m
⊢ IsUnit [].prod

Tactic:
simp

Result:
no goals