harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem cos_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : Real.Angle.cos (o.oangle y (y - x)) * ‖y - x‖ = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle y (y - x)).cos * ‖y - x‖ = ‖y‖

Tactic:
have hs : (o.oangle y (y - x)).sign = 1 := by
  rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ (o.oangle y (y - x)).cos * ‖y - x‖ = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ (o.oangle y (y - x)).cos * ‖y - x‖ = ‖y‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
  InnerProductGeometry.cos_angle_sub_mul_norm_of_inner_eq_zero
    (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle y (y - x)).sign = 1

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

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem coe_inv_le : (↑r⁻¹ : ℝ≥0∞) ≤ (↑r)⁻¹ :=
  le_sInf fun b (hb : 1 ≤ ↑r * b) =>
    coe_le_iff.2 <| by
      rintro b rfl
      apply NNReal.inv_le_of_le_mul
      rwa [← coe_mul, ← coe_one, coe_le_coe] at hb

Proof state:
r : ℝ≥0
b : ℝ≥0∞
hb : 1 ≤ ↑r * b
⊢ ∀ (p : ℝ≥0), b = ↑p → r⁻¹ ≤ p

Tactic:
rintro b rfl

Result:
r b : ℝ≥0
hb : 1 ≤ ↑r * ↑b
⊢ r⁻¹ ≤ b

Proof state:
r b : ℝ≥0
hb : 1 ≤ ↑r * ↑b
⊢ r⁻¹ ≤ b

Tactic:
apply NNReal.inv_le_of_le_mul

Result:
case h
r b : ℝ≥0
hb : 1 ≤ ↑r * ↑b
⊢ 1 ≤ r * b

Proof state:
case h
r b : ℝ≥0
hb : 1 ≤ ↑r * ↑b
⊢ 1 ≤ r * b

Tactic:
rwa [← coe_mul, ← coe_one, coe_le_coe] at hb

Result:
no goals
-- Mathlib/Order/CompleteLattice/Finset.lean
theorem iSup_finset_image {f : γ → α} {g : α → β} {s : Finset γ} :
    ⨆ x ∈ s.image f, g x = ⨆ y ∈ s, g (f y)

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
f : γ → α
g : α → β
s : Finset γ
⊢ ⨆ x ∈ image f s, g x = ⨆ y ∈ s, g (f y)

Tactic:
rw [← iSup_coe, coe_image, iSup_image, iSup_coe]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
theorem add_eq_coe :
    ∀ {a b : WithTop α} {c : α}, a + b = c ↔ ∃ a' b' : α, ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
  | ⊤, b, c => by simp
  | some a, ⊤, c => by simp
  | some a, some b, c => by norm_cast; simp

Proof state:
α : Type u
inst✝ : Add α
a b c : α
⊢ ↑a + ↑b = ↑c ↔ ∃ a' b', ↑a' = ↑a ∧ ↑b' = ↑b ∧ a' + b' = c

Tactic:
norm_cast

Result:
α : Type u
inst✝ : Add α
a b c : α
⊢ a + b = c ↔ ∃ a' b', a' = a ∧ b' = b ∧ a' + b' = c

Proof state:
α : Type u
inst✝ : Add α
a b c : α
⊢ a + b = c ↔ ∃ a' b', a' = a ∧ b' = b ∧ a' + b' = c

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝ : Add α
b : WithTop α
c : α
⊢ ⊤ + b = ↑c ↔ ∃ a' b', ↑a' = ⊤ ∧ ↑b' = b ∧ a' + b' = c

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝ : Add α
a c : α
⊢ ↑a + ⊤ = ↑c ↔ ∃ a' b', ↑a' = ↑a ∧ ↑b' = ⊤ ∧ a' + b' = c

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem conjugate {x : R} (hx : x ∈ skewAdjoint R) (z : R) : z * x * star z ∈ skewAdjoint R

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : x ∈ skewAdjoint R
z : R
⊢ z * x * star z ∈ skewAdjoint R

Tactic:
simp only [mem_iff, star_mul, star_star, mem_iff.mp hx, neg_mul, mul_neg, mul_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem add_eq_xor {a b : BitVec 1} : a + b = a ^^^ b

Proof state:
a b : BitVec 1
ha : a = 0 ∨ a = 1
⊢ a + b = a ^^^ b

Tactic:
have hb : b = 0 ∨ b = 1 := eq_zero_or_eq_one _

Result:
a b : BitVec 1
ha : a = 0 ∨ a = 1
hb : b = 0 ∨ b = 1
⊢ a + b = a ^^^ b

Proof state:
case inr
a b : BitVec 1
hb : b = 0 ∨ b = 1
h : a = 1
⊢ a + b = a ^^^ b

Tactic:
rcases hb with h' | h' <;> (simp [h, h'])

Result:
no goals

Proof state:
a b : BitVec 1
⊢ a + b = a ^^^ b

Tactic:
have ha : a = 0 ∨ a = 1 := eq_zero_or_eq_one _

Result:
a b : BitVec 1
ha : a = 0 ∨ a = 1
⊢ a + b = a ^^^ b

Proof state:
case inr.inr
a b : BitVec 1
h : a = 1
h' : b = 1
⊢ a + b = a ^^^ b

Tactic:
simp [h, h']

Result:
no goals

Proof state:
a b : BitVec 1
ha : a = 0 ∨ a = 1
hb : b = 0 ∨ b = 1
⊢ a + b = a ^^^ b

Tactic:
rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem isPeriodicPt_prod_map (x : α × β) :
    IsPeriodicPt (Prod.map f g) n x ↔ IsPeriodicPt f n x.1 ∧ IsPeriodicPt g n x.2

Proof state:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
n : ℕ
x : α × β
⊢ IsPeriodicPt (Prod.map f g) n x ↔ IsPeriodicPt f n x.1 ∧ IsPeriodicPt g n x.2

Tactic:
simp [IsPeriodicPt]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem whiskerLeft_rightUnitor_inv (f : a ⟶ b) (g : b ⟶ c) :
    f ◁ (ρ_ g).inv = (ρ_ (f ≫ g)).inv ≫ (α_ f g (𝟙 c)).hom :=
  eq_of_inv_eq_inv (by simp)

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ inv (f ◁ (ρ_ g).inv) = inv ((ρ_ (f ≫ g)).inv ≫ (α_ f g (𝟙 c)).hom)

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Group/Convolution.lean
theorem add_mconv [MeasurableMul₂ M] (μ : Measure M) (ν : Measure M) (ρ : Measure M) [SFinite μ]
    [SFinite ν] [SFinite ρ] : (μ + ν) ∗ ρ = μ ∗ ρ + ν ∗ ρ

Proof state:
M : Type u_1
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableSpace M
inst✝³ : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝² : SFinite μ
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
⊢ (μ + ν) ∗ ρ = μ ∗ ρ + ν ∗ ρ

Tactic:
unfold mconv

Result:
M : Type u_1
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableSpace M
inst✝³ : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝² : SFinite μ
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
⊢ map (fun x => x.1 * x.2) ((μ + ν).prod ρ) = map (fun x => x.1 * x.2) (μ.prod ρ) + map (fun x => x.1 * x.2) (ν.prod ρ)

Proof state:
case hf
M : Type u_1
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableSpace M
inst✝³ : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝² : SFinite μ
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
⊢ Measurable fun x => x.1 * x.2

Tactic:
fun_prop

Result:
no goals

Proof state:
M : Type u_1
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableSpace M
inst✝³ : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝² : SFinite μ
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
⊢ map (fun x => x.1 * x.2) ((μ + ν).prod ρ) = map (fun x => x.1 * x.2) (μ.prod ρ) + map (fun x => x.1 * x.2) (ν.prod ρ)

Tactic:
rw [add_prod, map_add]

Result:
case hf
M : Type u_1
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableSpace M
inst✝³ : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝² : SFinite μ
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
⊢ Measurable fun x => x.1 * x.2
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem Filter.HasBasis.uniformity_of_nhds_one_swapped {ι} {p : ι → Prop} {U : ι → Set α}
    (h : (𝓝 (1 : α)).HasBasis p U) :
    (𝓤 α).HasBasis p fun i => { x : α × α | x.1 / x.2 ∈ U i }

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (Filter.comap (fun x => x.1 / x.2) (𝓝 1)).HasBasis p fun i => {x | x.1 / x.2 ∈ U i}

Tactic:
exact h.comap _

Result:
no goals

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (𝓤 α).HasBasis p fun i => {x | x.1 / x.2 ∈ U i}

Tactic:
rw [uniformity_eq_comap_nhds_one_swapped]

Result:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (Filter.comap (fun x => x.1 / x.2) (𝓝 1)).HasBasis p fun i => {x | x.1 / x.2 ∈ U i}
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_comp_div_sub (hc : c ≠ 0) (d) :
    (∫ x in a..b, f (x / c - d)) = c • ∫ x in a / c - d..b / c - d, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (x / c - d) = c • ∫ (x : ℝ) in a / c - d..b / c - d, f x

Tactic:
simpa only [div_eq_inv_mul, inv_inv] using integral_comp_mul_sub f (inv_ne_zero hc) d

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
lemma triangle_aux₃ {X Y  : LocalizedMonoidal L W ε} {X' Y' : C}
    (e₁ : (L').obj X' ≅ X) (e₂ : (L').obj Y' ≅ Y) : (ρ_ X).hom ▷ _ =
      ((e₁.inv ⊗ ε.inv) ⊗ e₂.inv) ≫ _ ◁ e₂.hom ≫ ((μ L W ε X' (𝟙_ C)).hom ≫
        (L').map (ρ_ X').hom) ▷ Y ≫ e₁.hom ▷ Y

Proof state:
case e_f
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ (ρ_ X).hom = (e₁.inv ⊗ ε.inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom ≫ e₁.hom

Tactic:
rw [← cancel_mono e₁.inv, assoc, assoc, assoc, Iso.hom_inv_id, comp_id,
  ← rightUnitor_naturality, rightUnitor_hom_app,
  ← tensorHom_id, ← id_tensorHom, ← tensor_comp_assoc, comp_id, id_comp]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ (ρ_ X).hom ⊗ 𝟙 Y = (e₁.inv ⊗ ε.inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom ≫ e₁.hom ⊗ 𝟙 Y

Tactic:
congr

Result:
case e_f
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ (ρ_ X).hom = (e₁.inv ⊗ ε.inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom ≫ e₁.hom

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ (ρ_ X).hom ▷ Y =
    ((e₁.inv ⊗ ε.inv) ⊗ e₂.inv) ≫
      (L'.obj X' ⊗ L.obj (𝟙_ C)) ◁ e₂.hom ≫ ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ Y ≫ e₁.hom ▷ Y

Tactic:
simp only [← tensorHom_id, ← id_tensorHom, ← tensor_comp, assoc, comp_id,
  id_comp, Iso.inv_hom_id]

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ (ρ_ X).hom ⊗ 𝟙 Y = (e₁.inv ⊗ ε.inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom ≫ e₁.hom ⊗ 𝟙 Y
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_congr_left (hT : DominatedFinMeasAdditive μ T C)
    (hT' : DominatedFinMeasAdditive μ T' C') (h : T = T') (f : α → E) :
    setToFun μ T hT f = setToFun μ T' hT' f

Proof state:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : α → E
hf : Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
simp_rw [setToFun_eq _ hf, L1.setToL1_congr_left T T' hT hT' h]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : α → E
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
by_cases hf : Integrable f μ

Result:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : α → E
hf : Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T' hT' f

case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : α → E
hf : ¬Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Proof state:
case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : α → E
hf : ¬Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
simp_rw [setToFun_undef _ hf]

Result:
no goals
-- Mathlib/Tactic/NormNum/DivMod.lean
lemma isInt_emod_neg {a b : ℤ} {r : ℕ} (h : IsNat (a % -b) r) : IsNat (a % b) r :=
  ⟨by rw [← Int.emod_neg, h.out]⟩

Proof state:
a b : ℤ
r : ℕ
h : IsNat (a % -b) r
⊢ a % b = ↑r

Tactic:
rw [← Int.emod_neg, h.out]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup'_inf_distrib_left (f : ι → α) (a : α) :
    a ⊓ s.sup' hs f = s.sup' hs fun i ↦ a ⊓ f i

Proof state:
α : Type u_2
ι : Type u_5
inst✝ : DistribLattice α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ a ⊓ s.sup' hs f = s.sup' hs fun i => a ⊓ f i

Tactic:
induction hs using Finset.Nonempty.cons_induction with
| singleton => simp
| cons _ _ _ hs ih => simp_rw [sup'_cons hs, inf_sup_left, ih]

Result:
no goals

Proof state:
case cons
α : Type u_2
ι : Type u_5
inst✝ : DistribLattice α
s : Finset ι
hs✝ : s.Nonempty
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs : s✝.Nonempty
ih : a ⊓ s✝.sup' hs f = s✝.sup' hs fun i => a ⊓ f i
⊢ a ⊓ (cons a✝ s✝ h✝).sup' ⋯ f = (cons a✝ s✝ h✝).sup' ⋯ fun i => a ⊓ f i

Tactic:
simp_rw [sup'_cons hs, inf_sup_left, ih]

Result:
no goals

Proof state:
case singleton
α : Type u_2
ι : Type u_5
inst✝ : DistribLattice α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
a✝ : ι
⊢ a ⊓ {a✝}.sup' ⋯ f = {a✝}.sup' ⋯ fun i => a ⊓ f i

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Support.lean
theorem card_support_C_mul_X_pow_le_one {c : R} {n : ℕ} : #(support (C c * X ^ n)) ≤ 1

Proof state:
R : Type u
inst✝ : Semiring R
c : R
n : ℕ
⊢ #(C c * X ^ n).support ≤ 1

Tactic:
rw [← card_singleton n]

Result:
R : Type u
inst✝ : Semiring R
c : R
n : ℕ
⊢ #(C c * X ^ n).support ≤ #{n}

Proof state:
R : Type u
inst✝ : Semiring R
c : R
n : ℕ
⊢ #(C c * X ^ n).support ≤ #{n}

Tactic:
apply card_le_card (support_C_mul_X_pow' n c)

Result:
no goals
-- Mathlib/Data/Set/Sups.lean
lemma sep_infs_le (s t : Set α) (a : α) :
    {b ∈ s ⊼ t | a ≤ b} = {b ∈ s | a ≤ b} ⊼ {b ∈ t | a ≤ b}

Proof state:
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ {b | b ∈ s ⊼ t ∧ a ≤ b} = {b | b ∈ s ∧ a ≤ b} ⊼ {b | b ∈ t ∧ a ≤ b}

Tactic:
ext

Result:
case h
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a x✝ : α
⊢ x✝ ∈ {b | b ∈ s ⊼ t ∧ a ≤ b} ↔ x✝ ∈ {b | b ∈ s ∧ a ≤ b} ⊼ {b | b ∈ t ∧ a ≤ b}

Proof state:
case h
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a x✝ : α
⊢ x✝ ∈ {b | b ∈ s ⊼ t ∧ a ≤ b} ↔ x✝ ∈ {b | b ∈ s ∧ a ≤ b} ⊼ {b | b ∈ t ∧ a ≤ b}

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Module/End.lean
/-- `zsmul` is equal to any other module structure via a cast. -/
@[norm_cast]
lemma Int.cast_smul_eq_zsmul (n : ℤ) (b : M) : (n : R) • b = n • b :=
  have : ((smulAddHom R M).flip b).comp (Int.castAddHom R) = (smulAddHom ℤ M).flip b

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℤ
b : M
⊢ ((smulAddHom R M).flip b).comp (castAddHom R) = (smulAddHom ℤ M).flip b

Tactic:
apply AddMonoidHom.ext_int

Result:
case h1
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℤ
b : M
⊢ (((smulAddHom R M).flip b).comp (castAddHom R)) 1 = ((smulAddHom ℤ M).flip b) 1

Proof state:
case h1
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℤ
b : M
⊢ (((smulAddHom R M).flip b).comp (castAddHom R)) 1 = ((smulAddHom ℤ M).flip b) 1

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem orbit.eq_or_disjoint (a b : X) :
    orbit G a = orbit G b ∨ Disjoint (orbit G a) (orbit G b)

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a b : X
⊢ ¬Disjoint (orbit G a) (orbit G b) → orbit G a = orbit G b

Tactic:
simp +contextual
  only [Set.not_disjoint_iff, ← orbit_eq_iff, forall_exists_index, and_imp, eq_comm, implies_true]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a b : X
⊢ orbit G a = orbit G b ∨ Disjoint (orbit G a) (orbit G b)

Tactic:
apply (em (Disjoint (orbit G a) (orbit G b))).symm.imp _ id

Result:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a b : X
⊢ ¬Disjoint (orbit G a) (orbit G b) → orbit G a = orbit G b
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem IsNormal.conj' {S : Subgroupoid C} (Sn : IsNormal S) :
    ∀ {c d} (p : d ⟶ c) {γ : c ⟶ c}, γ ∈ S.arrows c c → p ≫ γ ≫ Groupoid.inv p ∈ S.arrows d d :=
  fun p γ hs => by convert Sn.conj (Groupoid.inv p) hs; simp

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c✝ d✝ : C
p : d✝ ⟶ c✝
γ : c✝ ⟶ c✝
hs : γ ∈ S.arrows c✝ c✝
⊢ p ≫ γ ≫ Groupoid.inv p ∈ S.arrows d✝ d✝

Tactic:
convert Sn.conj (Groupoid.inv p) hs

Result:
case h.e'_5.h.e'_6
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c✝ d✝ : C
p : d✝ ⟶ c✝
γ : c✝ ⟶ c✝
hs : γ ∈ S.arrows c✝ c✝
⊢ p = Groupoid.inv (Groupoid.inv p)

Proof state:
case h.e'_5.h.e'_6
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c✝ d✝ : C
p : d✝ ⟶ c✝
γ : c✝ ⟶ c✝
hs : γ ∈ S.arrows c✝ c✝
⊢ p = Groupoid.inv (Groupoid.inv p)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eval_nodal_derivative_eval_node_eq [DecidableEq ι] {i : ι} (hi : i ∈ s) :
    eval (v i) (derivative (nodal s v)) = eval (v i) (nodal (s.erase i) v)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
hi : i ∈ s
⊢ ∑ x ∈ s.erase i, eval (v i) (nodal (s.erase x) v) = 0

Tactic:
exact sum_eq_zero fun j hj => (eval_nodal_at_node (mem_erase.mpr ⟨(mem_erase.mp hj).1.symm, hi⟩))

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
hi : i ∈ s
⊢ eval (v i) (derivative (nodal s v)) = eval (v i) (nodal (s.erase i) v)

Tactic:
rw [derivative_nodal, eval_finset_sum, ← add_sum_erase _ _ hi, add_right_eq_self]

Result:
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
hi : i ∈ s
⊢ ∑ x ∈ s.erase i, eval (v i) (nodal (s.erase x) v) = 0
-- Mathlib/Order/KrullDimension.lean
/--
The coheight of an element in a series is larger or equal to its reverse index in the series.
-/
lemma rev_index_le_coheight (p : LTSeries α) (i : Fin (p.length + 1)) : i.rev ≤ coheight (p i)

Proof state:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
i : Fin (p.length + 1)
⊢ ↑↑i.rev ≤ coheight (p.toFun i)

Tactic:
simpa using index_le_height (α := αᵒᵈ) p.reverse i.rev

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_insert [LawfulBEq α] (h : m.WF) {a k : α} {v : β k} : (m.insert k v).get? a =
    if h : k == a then some (cast (congrArg β (eq_of_beq h)) v) else m.get? a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
a k : α
v : β k
⊢ (m.insert k v).get? a = if h : (k == a) = true then some (cast ⋯ v) else m.get? a

Tactic:
simp_to_raw using Raw₀.get?_insert

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Ring.lean
theorem cancel_right {f₁ f₂ : β →+*o γ} {g : α →+*o β} (hg : Surjective g) :
    f₁.comp g = f₂.comp g ↔ f₁ = f₂ :=
  ⟨fun h => ext <| hg.forall.2 <| DFunLike.ext_iff.1 h, fun h => by rw [h]⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : NonAssocSemiring α
inst✝⁴ : Preorder α
inst✝³ : NonAssocSemiring β
inst✝² : Preorder β
inst✝¹ : NonAssocSemiring γ
inst✝ : Preorder γ
f₁ f₂ : β →+*o γ
g : α →+*o β
hg : Surjective ⇑g
h : f₁ = f₂
⊢ f₁.comp g = f₂.comp g

Tactic:
rw [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem neg_lt_of_neg_lt {a b : Int} (h : -a < b) : -b < a

Proof state:
a b : Int
h : -a < b
⊢ -b < a

Tactic:
have h := Int.neg_lt_neg h

Result:
a b : Int
h✝ : -a < b
h : -b < - -a
⊢ -b < a

Proof state:
a b : Int
h✝ : -a < b
h : -b < - -a
⊢ -b < a

Tactic:
rwa [Int.neg_neg] at h

Result:
no goals