harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem oangle_rotation_right {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) (θ : Real.Angle) :
    o.oangle x (o.rotation θ y) = o.oangle x y + θ

Proof state:
case hy
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ (o.kahler x) y ≠ 0

Tactic:
exact o.kahler_ne_zero hx hy

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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ o.oangle x ((o.rotation θ) y) = o.oangle x y + θ

Tactic:
simp only [oangle, o.kahler_rotation_right]

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ ↑(↑θ.toCircle * (o.kahler x) y).arg = ↑((o.kahler x) y).arg + θ

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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ ↑(↑θ.toCircle * (o.kahler x) y).arg = ↑((o.kahler x) y).arg + θ

Tactic:
rw [Complex.arg_mul_coe_angle, Real.Angle.arg_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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ θ + ↑((o.kahler x) y).arg = ↑((o.kahler x) y).arg + θ

case hx
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ ↑θ.toCircle ≠ 0

case hy
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ (o.kahler x) y ≠ 0

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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ θ + ↑((o.kahler x) y).arg = ↑((o.kahler x) y).arg + θ

Tactic:
abel

Result:
no goals

Proof state:
case hx
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ ↑θ.toCircle ≠ 0

Tactic:
exact Circle.coe_ne_zero _

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean
/-- If we take the path along the spine of the `j`th face of a `spineToSimplex`,
a vertex `i` with `i ≥ j` can be identified with vertex `i + 1` in the original
path. -/
lemma spine_δ_vertex_ge (f : Path X (n + 1)) {i : Fin (n + 1)} {j : Fin (n + 2)}
    (h : j ≤ i.castSucc) :
    (X.spine n (X.δ j (spineToSimplex f))).vertex i = f.vertex i.succ

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : j ≤ i.castSucc
⊢ X.map (⦋0⦌.const ⦋n⦌ i).op (X.map (SimplexCategory.δ j).op (spineToSimplex f)) = f.vertex i.succ

Tactic:
rw [← FunctorToTypes.map_comp_apply, ← op_comp, SimplexCategory.const_comp,
  spineToSimplex_vertex]

Result:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : j ≤ i.castSucc
⊢ f.vertex ((Hom.toOrderHom (SimplexCategory.δ j)) i) = f.vertex i.succ

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : j ≤ i.castSucc
⊢ f.vertex ((Hom.toOrderHom (SimplexCategory.δ j)) i) = f.vertex i.succ

Tactic:
simp only [SimplexCategory.δ, Hom.toOrderHom, len_mk, mkHom, Hom.mk,
  OrderEmbedding.toOrderHom_coe, Fin.succAboveOrderEmb_apply]

Result:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : j ≤ i.castSucc
⊢ f.vertex (j.succAbove i) = f.vertex i.succ

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : j ≤ i.castSucc
⊢ f.vertex (j.succAbove i) = f.vertex i.succ

Tactic:
rw [Fin.succAbove_of_le_castSucc j i h]

Result:
no goals

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : j ≤ i.castSucc
⊢ (X.spine n (SimplicialObject.δ X j (spineToSimplex f))).vertex i = f.vertex i.succ

Tactic:
simp only [SimplicialObject.δ, spine_vertex]

Result:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : j ≤ i.castSucc
⊢ X.map (⦋0⦌.const ⦋n⦌ i).op (X.map (SimplexCategory.δ j).op (spineToSimplex f)) = f.vertex i.succ
-- Mathlib/Probability/Kernel/Basic.lean
theorem lintegral_piecewise (a : α) (g : β → ℝ≥0∞) :
    ∫⁻ b, g b ∂piecewise hs κ η a = if a ∈ s then ∫⁻ b, g b ∂κ a else ∫⁻ b, g b ∂η a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → ℝ≥0∞
⊢ ∫⁻ (b : β), g b ∂(piecewise hs κ η) a = if a ∈ s then ∫⁻ (b : β), g b ∂κ a else ∫⁻ (b : β), g b ∂η a

Tactic:
simp_rw [piecewise_apply]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → ℝ≥0∞
⊢ (∫⁻ (b : β), g b ∂if a ∈ s then κ a else η a) = if a ∈ s then ∫⁻ (b : β), g b ∂κ a else ∫⁻ (b : β), g b ∂η a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → ℝ≥0∞
⊢ (∫⁻ (b : β), g b ∂if a ∈ s then κ a else η a) = if a ∈ s then ∫⁻ (b : β), g b ∂κ a else ∫⁻ (b : β), g b ∂η a

Tactic:
split_ifs <;> rfl

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
theorem iIndepSet.meas_biInter {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω}
    {μ : Measure α} {f : ι → Set Ω} (h : iIndepSet f κ μ) (s : Finset ι) :
    ∀ᵐ a ∂μ, κ a (⋂ i ∈ s, f i) = ∏ i ∈ s, κ a (f i) :=
  iIndep.iIndepSets (fun _ ↦ rfl) h _ (by simp)

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : ι → Set Ω
h : iIndepSet f κ μ
s : Finset ι
⊢ ∀ i ∈ s, f i ∈ {f i}

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
@[simp]
lemma compProd_apply_univ [SFinite μ] [IsMarkovKernel κ] : (μ ⊗ₘ κ) univ = μ univ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsMarkovKernel κ
⊢ (μ ⊗ₘ κ) univ = μ univ

Tactic:
simp [compProd]

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
@[reassoc]
lemma whiskerLeft_curry'_comp {X Y Z : C} [Closed X] [Closed Y] (f : Y ⟶ Z) :
    _ ◁ curry' f ≫ comp X Y Z = (ρ_ _).hom ≫ (ihom X).map f

Proof state:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ X ◁ (ρ_ ((ihom X).obj Y)).inv ≫
      (α_ X ((ihom X).obj Y) (𝟙_ C)).inv ≫ (ihom.ev X).app Y ▷ 𝟙_ C ≫ Y ◁ curry' f ≫ (ihom.ev Y).app Z =
    (ihom.ev X).app Y ≫ f

Tactic:
rw [whiskerLeft_curry'_ihom_ev_app, whiskerLeft_rightUnitor_inv,
  MonoidalCategory.whiskerRight_id_assoc, Category.assoc,
  Iso.inv_hom_id_assoc, Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc,]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ (ρ_ ((ihom X).obj Y)).inv ≫ (ihom X).obj Y ◁ curry' f ≫ comp X Y Z = (ihom X).map f

Tactic:
apply uncurry_injective

Result:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ uncurry ((ρ_ ((ihom X).obj Y)).inv ≫ (ihom X).obj Y ◁ curry' f ≫ comp X Y Z) = uncurry ((ihom X).map f)

Proof state:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ uncurry ((ρ_ ((ihom X).obj Y)).inv ≫ (ihom X).obj Y ◁ curry' f ≫ comp X Y Z) = uncurry ((ihom X).map f)

Tactic:
rw [uncurry_ihom_map, comp_eq, ← curry_natural_left, ← curry_natural_left, uncurry_curry,
  compTranspose_eq, associator_inv_naturality_right_assoc, whisker_exchange_assoc]

Result:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ X ◁ (ρ_ ((ihom X).obj Y)).inv ≫
      (α_ X ((ihom X).obj Y) (𝟙_ C)).inv ≫ (ihom.ev X).app Y ▷ 𝟙_ C ≫ (𝟭 C).obj Y ◁ curry' f ≫ (ihom.ev Y).app Z =
    (ihom.ev X).app Y ≫ f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ (ihom X).obj Y ◁ curry' f ≫ comp X Y Z = (ρ_ ((ihom X).obj Y)).hom ≫ (ihom X).map f

Tactic:
rw [← cancel_epi (ρ_ _).inv, Iso.inv_hom_id_assoc]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ (ρ_ ((ihom X).obj Y)).inv ≫ (ihom X).obj Y ◁ curry' f ≫ comp X Y Z = (ihom X).map f

Proof state:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ X ◁ (ρ_ ((ihom X).obj Y)).inv ≫
      (α_ X ((ihom X).obj Y) (𝟙_ C)).inv ≫ (ihom.ev X).app Y ▷ 𝟙_ C ≫ (𝟭 C).obj Y ◁ curry' f ≫ (ihom.ev Y).app Z =
    (ihom.ev X).app Y ≫ f

Tactic:
dsimp

Result:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ X ◁ (ρ_ ((ihom X).obj Y)).inv ≫
      (α_ X ((ihom X).obj Y) (𝟙_ C)).inv ≫ (ihom.ev X).app Y ▷ 𝟙_ C ≫ Y ◁ curry' f ≫ (ihom.ev Y).app Z =
    (ihom.ev X).app Y ≫ f
-- Mathlib/Algebra/Module/Torsion.lean
theorem torsionBy_le_torsionBy_of_dvd (a b : R) (dvd : a ∣ b) :
    torsionBy R M a ≤ torsionBy R M b

Proof state:
case st
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a c : R
dvd : a ∣ c
⊢ c ∈ ↑(span R {a})

Tactic:
exact Ideal.mem_span_singleton.mpr dvd

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : R
dvd : a ∣ b
⊢ torsionBy R M a ≤ torsionBy R M b

Tactic:
rw [← torsionBySet_span_singleton_eq, ← torsionBySet_singleton_eq]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : R
dvd : a ∣ b
⊢ torsionBySet R M ↑(span R {a}) ≤ torsionBySet R M {b}

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : R
dvd : a ∣ b
⊢ torsionBySet R M ↑(span R {a}) ≤ torsionBySet R M {b}

Tactic:
apply torsionBySet_le_torsionBySet_of_subset

Result:
case st
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : R
dvd : a ∣ b
⊢ {b} ⊆ ↑(span R {a})

Proof state:
case st
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : R
dvd : a ∣ b
⊢ {b} ⊆ ↑(span R {a})

Tactic:
rintro c (rfl : c = b)

Result:
case st
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a c : R
dvd : a ∣ c
⊢ c ∈ ↑(span R {a})
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem continuous {f : α → β} (hf : LocallyLipschitz f) : Continuous f

Proof state:
case intro.intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : LocallyLipschitz f
x : α
K : ℝ≥0
t : Set α
ht : t ∈ 𝓝 x
hK : LipschitzOnWith K f t
⊢ ContinuousAt f x

Tactic:
exact (hK.continuousOn).continuousAt ht

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : LocallyLipschitz f
⊢ Continuous f

Tactic:
rw [continuous_iff_continuousAt]

Result:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : LocallyLipschitz f
⊢ ∀ (x : α), ContinuousAt f x

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : LocallyLipschitz f
⊢ ∀ (x : α), ContinuousAt f x

Tactic:
intro x

Result:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : LocallyLipschitz f
x : α
⊢ ContinuousAt f x

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : LocallyLipschitz f
x : α
⊢ ContinuousAt f x

Tactic:
rcases (hf x) with ⟨K, t, ht, hK⟩

Result:
case intro.intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : LocallyLipschitz f
x : α
K : ℝ≥0
t : Set α
ht : t ∈ 𝓝 x
hK : LipschitzOnWith K f t
⊢ ContinuousAt f x
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem lTensor_comp_rTensor (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    (g.lTensor P).comp (f.rTensor N) = map f g

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ lTensor P g ∘ₗ rTensor N f = map f g

Tactic:
simp only [lTensor, rTensor, ← map_comp, id_comp, comp_id]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean
theorem Group.covariant_swap_iff_contravariant_swap [Group N] :
    Covariant N N (swap (· * ·)) r ↔ Contravariant N N (swap (· * ·)) r

Proof state:
case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (swap fun x1 x2 => x1 * x2) r
a b c : N
bc : r (swap (fun x1 x2 => x1 * x2) a b) (swap (fun x1 x2 => x1 * x2) a c)
⊢ r b c

Tactic:
rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a]

Result:
case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (swap fun x1 x2 => x1 * x2) r
a b c : N
bc : r (swap (fun x1 x2 => x1 * x2) a b) (swap (fun x1 x2 => x1 * x2) a c)
⊢ r (b * a * a⁻¹) (c * a * a⁻¹)

Proof state:
case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (swap fun x1 x2 => x1 * x2) r
a b c : N
bc : r (b * a * a⁻¹) (c * a * a⁻¹)
⊢ r (swap (fun x1 x2 => x1 * x2) a b) (swap (fun x1 x2 => x1 * x2) a c)

Tactic:
exact h a⁻¹ bc

Result:
no goals

Proof state:
N : Type u_2
r : N → N → Prop
inst✝ : Group N
⊢ Covariant N N (swap fun x1 x2 => x1 * x2) r ↔ Contravariant N N (swap fun x1 x2 => x1 * x2) r

Tactic:
refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩

Result:
case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (swap fun x1 x2 => x1 * x2) r
a b c : N
bc : r (swap (fun x1 x2 => x1 * x2) a b) (swap (fun x1 x2 => x1 * x2) a c)
⊢ r b c

case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (swap fun x1 x2 => x1 * x2) r
a b c : N
bc : r b c
⊢ r (swap (fun x1 x2 => x1 * x2) a b) (swap (fun x1 x2 => x1 * x2) a c)

Proof state:
case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (swap fun x1 x2 => x1 * x2) r
a b c : N
bc : r b c
⊢ r (swap (fun x1 x2 => x1 * x2) a b) (swap (fun x1 x2 => x1 * x2) a c)

Tactic:
rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a] at bc

Result:
case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (swap fun x1 x2 => x1 * x2) r
a b c : N
bc : r (b * a * a⁻¹) (c * a * a⁻¹)
⊢ r (swap (fun x1 x2 => x1 * x2) a b) (swap (fun x1 x2 => x1 * x2) a c)

Proof state:
case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (swap fun x1 x2 => x1 * x2) r
a b c : N
bc : r (swap (fun x1 x2 => x1 * x2) a b) (swap (fun x1 x2 => x1 * x2) a c)
⊢ r (b * a * a⁻¹) (c * a * a⁻¹)

Tactic:
exact h a⁻¹ bc

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Nat.lean
theorem f_inj {n : ℕ} (a : Fin 3 → ℕ) (ha : a ∈ finMulAntidiag 3 n)
    (b : Fin 3 → ℕ) (hb : b ∈ finMulAntidiag 3 n) (hfab : f a ha = f b hb) :
    a = b

Proof state:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : Nat.card_pair_lcm_eq.f a ha = Nat.card_pair_lcm_eq.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
⊢ a = b

Tactic:
have hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2 := by
  rw [finMulAntidiag_three a ha, hfab1, finMulAntidiag_three b hb]

Result:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : Nat.card_pair_lcm_eq.f a ha = Nat.card_pair_lcm_eq.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
⊢ a = b
-- Mathlib/LinearAlgebra/FreeModule/Determinant.lean
theorem LinearMap.det_zero'' {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
    [Module.Free R M] [Module.Finite R M] [Nontrivial M] : LinearMap.det (0 : M →ₗ[R] M) = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
⊢ LinearMap.det 0 = 0

Tactic:
letI : Nonempty (Module.Free.ChooseBasisIndex R M) := (Module.Free.chooseBasis R M).index_nonempty

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
this : Nonempty (Module.Free.ChooseBasisIndex R M) := Basis.index_nonempty (Module.Free.chooseBasis R M)
⊢ LinearMap.det 0 = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
this : Nonempty (Module.Free.ChooseBasisIndex R M) := Basis.index_nonempty (Module.Free.chooseBasis R M)
⊢ LinearMap.det 0 = 0

Tactic:
nontriviality R

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
this : Nonempty (Module.Free.ChooseBasisIndex R M) := Basis.index_nonempty (Module.Free.chooseBasis R M)
a✝ : Nontrivial R
⊢ LinearMap.det 0 = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
this : Nonempty (Module.Free.ChooseBasisIndex R M) := Basis.index_nonempty (Module.Free.chooseBasis R M)
a✝ : Nontrivial R
⊢ LinearMap.det 0 = 0

Tactic:
exact LinearMap.det_zero' (Module.Free.chooseBasis R M)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem count_eq_countP' {a : α} : count (n := n) a = countP (· == a)

Proof state:
case h
α : Type u_1
inst✝ : BEq α
n : Nat
a : α
l : Vector α n
⊢ count a l = countP (fun x => x == a) l

Tactic:
apply count_eq_countP

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
n : Nat
a : α
⊢ count a = countP fun x => x == a

Tactic:
funext l

Result:
case h
α : Type u_1
inst✝ : BEq α
n : Nat
a : α
l : Vector α n
⊢ count a l = countP (fun x => x == a) l
-- Mathlib/Data/Finset/Sups.lean
theorem disjSups_comm : s ○ t = t ○ s

Proof state:
case h.mpr.intro.intro.intro.intro.intro
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
a✝ a : α
ha : a ∈ t
b : α
hb : b ∈ s
hd : Disjoint b a
hs : a ⊔ b = a✝
⊢ ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = a✝

Tactic:
rw [sup_comm] at hs

Result:
case h.mpr.intro.intro.intro.intro.intro
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
a✝ a : α
ha : a ∈ t
b : α
hb : b ∈ s
hd : Disjoint b a
hs : b ⊔ a = a✝
⊢ ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = a✝

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ s ○ t = t ○ s

Tactic:
ext

Result:
case h
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
a✝ : α
⊢ a✝ ∈ s ○ t ↔ a✝ ∈ t ○ s

Proof state:
case h.mpr.intro.intro.intro.intro.intro
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
a✝ a : α
ha : a ∈ t
b : α
hb : b ∈ s
hd : Disjoint b a
hs : b ⊔ a = a✝
⊢ ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = a✝

Tactic:
exact ⟨b, hb, a, ha, hd, hs⟩

Result:
no goals

Proof state:
case h.mpr
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
a✝ : α
⊢ (∃ a ∈ t, ∃ b ∈ s, Disjoint a b ∧ a ⊔ b = a✝) → ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = a✝

Tactic:
rintro ⟨a, ha, b, hb, hd, hs⟩

Result:
case h.mpr.intro.intro.intro.intro.intro
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
a✝ a : α
ha : a ∈ t
b : α
hb : b ∈ s
hd : Disjoint a b
hs : a ⊔ b = a✝
⊢ ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = a✝

Proof state:
case h.mpr.intro.intro.intro.intro.intro
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
a✝ a : α
ha : a ∈ t
b : α
hb : b ∈ s
hd : Disjoint a b
hs : a ⊔ b = a✝
⊢ ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = a✝

Tactic:
rw [disjoint_comm] at hd

Result:
case h.mpr.intro.intro.intro.intro.intro
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
a✝ a : α
ha : a ∈ t
b : α
hb : b ∈ s
hd : Disjoint b a
hs : a ⊔ b = a✝
⊢ ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = a✝

Proof state:
case h
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
a✝ : α
⊢ a✝ ∈ s ○ t ↔ a✝ ∈ t ○ s

Tactic:
rw [mem_disjSups, mem_disjSups]

Result:
case h
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
a✝ : α
⊢ (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = a✝) ↔ ∃ a ∈ t, ∃ b ∈ s, Disjoint a b ∧ a ⊔ b = a✝
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem not_mem_support_iff {p : MvPolynomial σ R} {m : σ →₀ ℕ} : m ∉ p.support ↔ p.coeff m = 0 :=
  by simp

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ m ∉ p.support ↔ coeff m p = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arcsin_nonneg {x : ℝ} : 0 ≤ arcsin x ↔ 0 ≤ x :=
  (le_arcsin_iff_sin_le' ⟨neg_lt_zero.2 pi_div_two_pos, pi_div_two_pos.le⟩).trans <| by
    rw [sin_zero]

Proof state:
x : ℝ
⊢ sin 0 ≤ x ↔ 0 ≤ x

Tactic:
rw [sin_zero]

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem comap_map_eq_self {f : A →ₐ[R] B} {S : Subalgebra R A}
    (h : f ⁻¹' {0} ⊆ S) : (S.map f).comap f = S

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
h : ⇑f ⁻¹' {0} ⊆ ↑S
⊢ comap f (map f S) = S

Tactic:
convert comap_map_eq f S

Result:
case h.e'_3
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
h : ⇑f ⁻¹' {0} ⊆ ↑S
⊢ S = S ⊔ adjoin R (⇑f ⁻¹' {0})

Proof state:
case h.e'_3
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
h : ⇑f ⁻¹' {0} ⊆ ↑S
⊢ S = S ⊔ adjoin R (⇑f ⁻¹' {0})

Tactic:
rwa [left_eq_sup, Algebra.adjoin_le_iff]

Result:
no goals