harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Int/Lemmas.lean
theorem natAbs_inj_of_nonneg_of_nonpos {a b : ℤ} (ha : 0 ≤ a) (hb : b ≤ 0) :
    natAbs a = natAbs b ↔ a = -b

Proof state:
a b : ℤ
ha : 0 ≤ a
hb : b ≤ 0
⊢ a.natAbs = b.natAbs ↔ a = -b

Tactic:
simpa only [Int.natAbs_neg] using natAbs_inj_of_nonneg_of_nonneg ha (neg_nonneg_of_nonpos hb)

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem ball_eq' (y : E) (ε : ℝ) : ball y ε = { x | ‖x / y‖ < ε } :=
  Set.ext fun a => by simp [dist_eq_norm_div]

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
y : E
ε : ℝ
a : E
⊢ a ∈ ball y ε ↔ a ∈ {x | ‖x / y‖ < ε}

Tactic:
simp [dist_eq_norm_div]

Result:
no goals
-- Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean
theorem toFinsupp_of (x : X) : toFinsupp (of x) = Finsupp.single x 1

Proof state:
X : Type u_1
x : X
⊢ toFinsupp (of x) = single x 1

Tactic:
simp only [toFinsupp, lift.of]

Result:
no goals
-- Mathlib/Topology/Order/Monotone.lean
theorem Monotone.map_ciInf_of_continuousAt {ι : Sort*} [Nonempty ι] {f : α → β} {g : ι → α}
    (Cf : ContinuousAt f (iInf g)) (Mf : Monotone f)
    (bdd : BddBelow (range g)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Mf : Monotone f
bdd : autoParam (BddBelow (range g)) _auto✝
⊢ f (⨅ i, g i) = ⨅ i, f (g i)

Tactic:
rw [iInf, Monotone.map_csInf_of_continuousAt Cf Mf (range_nonempty g) bdd, ← range_comp, iInf,
  comp_def]

Result:
no goals
-- Mathlib/Probability/Kernel/Basic.lean
lemma lintegral_id [MeasurableSingletonClass α] {f : α → ℝ≥0∞} (a : α) :
    ∫⁻ a, f a ∂(@Kernel.id α mα a) = f a

Proof state:
α : Type u_1
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
⊢ ∫⁻ (a : α), f a ∂Kernel.id a = f a

Tactic:
rw [id_apply, lintegral_dirac]

Result:
no goals
-- Mathlib/LinearAlgebra/Orientation.lean
theorem orientation_comp_linearEquiv_eq_iff_det_pos (e : Basis ι R M) (f : M ≃ₗ[R] M) :
    (e.map f).orientation = e.orientation ↔ 0 < LinearMap.det (f : M →ₗ[R] M)

Proof state:
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
f : M ≃ₗ[R] M
⊢ (e.map f).orientation = e.orientation ↔ 0 < LinearMap.det ↑f

Tactic:
rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_self_iff,
  LinearEquiv.coe_det]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Rank.lean
theorem rank_sUnion_le (x : ZFSet) : rank (⋃₀ x) ≤ rank x

Proof state:
x : ZFSet.{u_1}
⊢ (⋃₀ x).rank ≤ x.rank

Tactic:
simp_rw [rank_le_iff, mem_sUnion]

Result:
x : ZFSet.{u_1}
⊢ ∀ ⦃y : ZFSet.{u_1}⦄, (∃ z ∈ x, y ∈ z) → y.rank < x.rank

Proof state:
x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝.rank < x.rank

Tactic:
trans <;> apply rank_lt_of_mem <;> assumption

Result:
no goals

Proof state:
x : ZFSet.{u_1}
⊢ ∀ ⦃y : ZFSet.{u_1}⦄, (∃ z ∈ x, y ∈ z) → y.rank < x.rank

Tactic:
intro _ ⟨_, _, _⟩

Result:
x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝.rank < x.rank
-- Mathlib/Data/ENNReal/Inv.lean
theorem add_thirds (a : ℝ≥0∞) : a / 3 + a / 3 + a / 3 = a

Proof state:
a : ℝ≥0∞
⊢ a / 3 + a / 3 + a / 3 = a

Tactic:
rw [div_eq_mul_inv, ← mul_add, ← mul_add, inv_three_add_inv_three, mul_one]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem ediam_eq {s : Set ℝ} (h : Bornology.IsBounded s) :
    EMetric.diam s = ENNReal.ofReal (sSup s - sInf s)

Proof state:
case inr.refine_2.h
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ sSup s - sInf s ≤ (EMetric.diam s).toReal

Tactic:
rw [← Metric.diam, ← Metric.diam_closure]

Result:
case inr.refine_2.h
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ sSup s - sInf s ≤ Metric.diam (closure s)

Proof state:
case inr.refine_2.h
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ sSup s - sInf s ≤ Metric.diam (closure s)

Tactic:
calc sSup s - sInf s ≤ dist (sSup s) (sInf s) := le_abs_self _
_ ≤ Metric.diam (closure s) := dist_le_diam_of_mem h.closure (csSup_mem_closure hne h.bddAbove)
    (csInf_mem_closure hne h.bddBelow)

Result:
no goals

Proof state:
case inl
h : Bornology.IsBounded ∅
⊢ EMetric.diam ∅ = ENNReal.ofReal (sSup ∅ - sInf ∅)

Tactic:
simp

Result:
no goals

Proof state:
case inr
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ EMetric.diam s = ENNReal.ofReal (sSup s - sInf s)

Tactic:
refine le_antisymm (Metric.ediam_le_of_forall_dist_le fun x hx y hy => ?_) ?_

Result:
case inr.refine_1
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
⊢ dist x y ≤ sSup s - sInf s

case inr.refine_2
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ ENNReal.ofReal (sSup s - sInf s) ≤ EMetric.diam s

Proof state:
case inr.refine_1
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
⊢ dist x y ≤ sSup s - sInf s

Tactic:
exact Real.dist_le_of_mem_Icc (h.subset_Icc_sInf_sSup hx) (h.subset_Icc_sInf_sSup hy)

Result:
no goals

Proof state:
case inr.refine_2
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ ENNReal.ofReal (sSup s - sInf s) ≤ EMetric.diam s

Tactic:
apply ENNReal.ofReal_le_of_le_toReal

Result:
case inr.refine_2.h
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ sSup s - sInf s ≤ (EMetric.diam s).toReal

Proof state:
s : Set ℝ
h : Bornology.IsBounded s
⊢ EMetric.diam s = ENNReal.ofReal (sSup s - sInf s)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hne)

Result:
case inl
h : Bornology.IsBounded ∅
⊢ EMetric.diam ∅ = ENNReal.ofReal (sSup ∅ - sInf ∅)

case inr
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ EMetric.diam s = ENNReal.ofReal (sSup s - sInf s)
-- Mathlib/Algebra/Category/Grp/Basic.lean
@[to_additive]
lemma ofHom_injective {X Y : Type u} [Group X] [Group Y] :
    Function.Injective (fun (f : X →* Y) ↦ ofHom f)

Proof state:
X Y : Type u
inst✝¹ : Group X
inst✝ : Group Y
a₁✝ a₂✝ : X →* Y
h : (fun f => ofHom f) a₁✝ = (fun f => ofHom f) a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext

Result:
case h
X Y : Type u
inst✝¹ : Group X
inst✝ : Group Y
a₁✝ a₂✝ : X →* Y
h : (fun f => ofHom f) a₁✝ = (fun f => ofHom f) a₂✝
x✝ : X
⊢ a₁✝ x✝ = a₂✝ x✝

Proof state:
X Y : Type u
inst✝¹ : Group X
inst✝ : Group Y
⊢ Function.Injective fun f => ofHom f

Tactic:
intro _ _ h

Result:
X Y : Type u
inst✝¹ : Group X
inst✝ : Group Y
a₁✝ a₂✝ : X →* Y
h : (fun f => ofHom f) a₁✝ = (fun f => ofHom f) a₂✝
⊢ a₁✝ = a₂✝

Proof state:
case h
X Y : Type u
inst✝¹ : Group X
inst✝ : Group Y
a₁✝ a₂✝ : X →* Y
h : (fun f => ofHom f) a₁✝ = (fun f => ofHom f) a₂✝
x✝ : X
⊢ a₁✝ x✝ = a₂✝ x✝

Tactic:
apply ConcreteCategory.congr_hom h

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
theorem hasProd_nat_add_iff {f : ℕ → G} (k : ℕ) :
    HasProd (fun n ↦ f (n + k)) g ↔ HasProd f (g * ∏ i ∈ range k, f i)

Proof state:
G : Type u_2
inst✝² : CommGroup G
g : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
k : ℕ
⊢ HasProd (fun n => f (n + k)) g ↔ HasProd f (g * ∏ i ∈ range k, f i)

Tactic:
refine Iff.trans ?_ (range k).hasProd_compl_iff

Result:
G : Type u_2
inst✝² : CommGroup G
g : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
k : ℕ
⊢ HasProd (fun n => f (n + k)) g ↔ HasProd (fun x => f ↑x) g

Proof state:
G : Type u_2
inst✝² : CommGroup G
g : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
k : ℕ
⊢ HasProd (fun n => f (n + k)) g ↔ HasProd (fun x => f ↑x) g

Tactic:
rw [← (notMemRangeEquiv k).symm.hasProd_iff, Function.comp_def, coe_notMemRangeEquiv_symm]

Result:
no goals
-- Mathlib/MeasureTheory/PiSystem.lean
theorem isPiSystem_Icc (f : ι → α) (g : ι' → α) :
    @IsPiSystem α { S | ∃ i j, f i ≤ g j ∧ Icc (f i) (g j) = S } :=
  isPiSystem_Ixx (Ixx := Icc) nonempty_Icc.1 (by exact Icc_inter_Icc) f g

Proof state:
α : Type u_1
ι : Sort u_3
ι' : Sort u_4
inst✝ : LinearOrder α
f : ι → α
g : ι' → α
⊢ ∀ {a₁ b₁ a₂ b₂ : α}, Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂)

Tactic:
exact Icc_inter_Icc

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem tan_div_sqrt_one_add_tan_sq {x : ℝ} (hx : 0 < cos x) :
    tan x / √(1 + tan x ^ 2) = sin x

Proof state:
x : ℝ
hx : 0 < cos x
⊢ tan x / √(1 + tan x ^ 2) = sin x

Tactic:
rw [← tan_mul_cos hx.ne', ← inv_sqrt_one_add_tan_sq hx, div_eq_mul_inv]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ae_restrict_uIoc_eq [LinearOrder α] (a b : α) :
    ae (μ.restrict (Ι a b)) = ae (μ.restrict (Ioc a b)) ⊔ ae (μ.restrict (Ioc b a))

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder α
a b : α
⊢ ae (μ.restrict (Ι a b)) = ae (μ.restrict (Ioc a b)) ⊔ ae (μ.restrict (Ioc b a))

Tactic:
simp only [uIoc_eq_union, ae_restrict_union_eq]

Result:
no goals
-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
lemma eventually_atTop_ge {b : ℝ} (hb : b ∈ Set.Ioo 0 1) (hf : GrowsPolynomially f) :
    ∃ c > 0, ∀ᶠ x in atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u

Proof state:
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
⊢ ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u

Tactic:
obtain ⟨c₁, hc₁, c₂, _, h⟩ := hf b hb

Result:
case intro.intro.intro.intro
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c₁ : ℝ
hc₁ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u

Proof state:
case intro.intro.intro.intro
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c₁ : ℝ
hc₁ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c₁ * f x ≤ f u

Tactic:
filter_upwards [h]

Result:
case h
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c₁ : ℝ
hc₁ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ (a : ℝ), (∀ u ∈ Set.Icc (b * a) a, f u ∈ Set.Icc (c₁ * f a) (c₂ * f a)) → ∀ u ∈ Set.Icc (b * a) a, c₁ * f a ≤ f u

Proof state:
case h
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c₁ : ℝ
hc₁ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ (a : ℝ), (∀ u ∈ Set.Icc (b * a) a, f u ∈ Set.Icc (c₁ * f a) (c₂ * f a)) → ∀ u ∈ Set.Icc (b * a) a, c₁ * f a ≤ f u

Tactic:
exact fun _ H u hu => (H u hu).1

Result:
no goals

Proof state:
case intro.intro.intro.intro
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c₁ : ℝ
hc₁ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u

Tactic:
refine ⟨c₁, hc₁, ?_⟩

Result:
case intro.intro.intro.intro
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c₁ : ℝ
hc₁ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c₁ * f x ≤ f u
-- Mathlib/Order/OmegaCompletePartialOrder.lean
lemma ωScottContinuous.prodMk (hf : ωScottContinuous f) (hg : ωScottContinuous g) :
    ωScottContinuous fun x => (f x, g x) := ScottContinuousOn.prodMk (fun a b hab => by
  use pair a b hab; exact range_pair a b hab) hf hg

Proof state:
case h
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
a b : α
hab : a ≤ b
⊢ (fun c => Set.range ⇑c) (pair a b hab) = {a, b}

Tactic:
exact range_pair a b hab

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
a b : α
hab : a ≤ b
⊢ {a, b} ∈ Set.range fun c => Set.range ⇑c

Tactic:
use pair a b hab

Result:
case h
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
a b : α
hab : a ≤ b
⊢ (fun c => Set.range ⇑c) (pair a b hab) = {a, b}
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem apply_ne_one_iff [MulZeroOneClass α] [Nontrivial α] (h : IsAdjMatrix A) (i j : V) :
    ¬A i j = 1 ↔ A i j = 0

Proof state:
V : Type u_1
α : Type u_2
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
i j : V
⊢ ¬A i j = 1 ↔ A i j = 0

Tactic:
obtain h | h := h.zero_or_one i j <;> simp [h]

Result:
no goals
-- Mathlib/GroupTheory/Goursat.lean
@[to_additive AddSubgroup.goursatFst_prod_goursatSnd_le]
lemma goursatFst_prod_goursatSnd_le : I.goursatFst.prod I.goursatSnd ≤ I

Proof state:
case mk.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
g : G
h : H
hg : (g, h).1 ∈ ↑I.goursatFst.toSubmonoid
hh : (g, h).2 ∈ ↑I.goursatSnd.toSubmonoid
⊢ (g, h) ∈ I

Tactic:
simpa using mul_mem (mem_goursatFst.1 hg) (mem_goursatSnd.1 hh)

Result:
no goals

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
⊢ I.goursatFst.prod I.goursatSnd ≤ I

Tactic:
rintro ⟨g, h⟩ ⟨hg, hh⟩

Result:
case mk.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
g : G
h : H
hg : (g, h).1 ∈ ↑I.goursatFst.toSubmonoid
hh : (g, h).2 ∈ ↑I.goursatSnd.toSubmonoid
⊢ (g, h) ∈ I
-- Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
theorem thickenedIndicator_one_of_mem_closure {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) {x : α}
    (x_mem : x ∈ closure E) : thickenedIndicator δ_pos E x = 1

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_mem : x ∈ closure E
⊢ (thickenedIndicator δ_pos E) x = 1

Tactic:
rw [thickenedIndicator_apply, thickenedIndicatorAux_one_of_mem_closure δ E x_mem, one_toNNReal]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem lift_normNoninc {N : Type*} [SeminormedAddCommGroup N] (S : AddSubgroup M)
    (f : NormedAddGroupHom M N) (hf : ∀ s ∈ S, f s = 0) (fb : f.NormNoninc) :
    (lift S f hf).NormNoninc := fun x => by
  have fb' : ‖f‖ ≤ (1 : ℝ≥0) := NormNoninc.normNoninc_iff_norm_le_one.mp fb
  simpa using le_of_opNorm_le _ (f.lift_norm_le _ _ fb') _

Proof state:
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, f s = 0
fb : f.NormNoninc
x : M ⧸ S
fb' : ‖f‖ ≤ ↑1
⊢ ‖(lift S f hf) x‖ ≤ ‖x‖

Tactic:
simpa using le_of_opNorm_le _ (f.lift_norm_le _ _ fb') _

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, f s = 0
fb : f.NormNoninc
x : M ⧸ S
⊢ ‖(lift S f hf) x‖ ≤ ‖x‖

Tactic:
have fb' : ‖f‖ ≤ (1 : ℝ≥0) := NormNoninc.normNoninc_iff_norm_le_one.mp fb

Result:
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, f s = 0
fb : f.NormNoninc
x : M ⧸ S
fb' : ‖f‖ ≤ ↑1
⊢ ‖(lift S f hf) x‖ ≤ ‖x‖
-- Mathlib/Data/PNat/Factors.lean
theorem prod_dvd_iff {u v : PrimeMultiset} : u.prod ∣ v.prod ↔ u ≤ v

Proof state:
u v : PrimeMultiset
h : u ≤ v ↔ u.prod ∣ v.prod
⊢ u.prod ∣ v.prod ↔ u ≤ v

Tactic:
exact h.symm

Result:
no goals

Proof state:
u v : PrimeMultiset
⊢ u.prod ∣ v.prod ↔ u ≤ v

Tactic:
let h := @PNat.factorMultiset_le_iff' u.prod v

Result:
u v : PrimeMultiset
h : u.prod.factorMultiset ≤ v ↔ u.prod ∣ v.prod := PNat.factorMultiset_le_iff'
⊢ u.prod ∣ v.prod ↔ u ≤ v

Proof state:
u v : PrimeMultiset
h : u.prod.factorMultiset ≤ v ↔ u.prod ∣ v.prod := PNat.factorMultiset_le_iff'
⊢ u.prod ∣ v.prod ↔ u ≤ v

Tactic:
rw [u.factorMultiset_prod] at h

Result:
u v : PrimeMultiset
h : u ≤ v ↔ u.prod ∣ v.prod
⊢ u.prod ∣ v.prod ↔ u ≤ v
-- Mathlib/GroupTheory/Exponent.lean
@[to_additive]
lemma mul_not_mem_of_orderOf_eq_two {x y : G} (hx : orderOf x = 2)
    (hy : orderOf y = 2) (hxy : x ≠ y) : x * y ∉ ({x, y, 1} : Set G)

Proof state:
G : Type u
inst✝ : Group G
x y : G
hx : orderOf x = 2
hy : orderOf y = 2
hxy : x ≠ y
⊢ x * y ∉ {x, y, 1}

Tactic:
simp only [Set.mem_singleton_iff, Set.mem_insert_iff, mul_right_eq_self, mul_left_eq_self,
  mul_eq_one_iff_eq_inv, inv_eq_self_of_orderOf_eq_two hy, not_or]

Result:
G : Type u
inst✝ : Group G
x y : G
hx : orderOf x = 2
hy : orderOf y = 2
hxy : x ≠ y
⊢ ¬y = 1 ∧ ¬x = 1 ∧ ¬x = y

Proof state:
G : Type u
inst✝ : Group G
x y : G
hx : orderOf x = 2
hy : orderOf y = 2
hxy : x ≠ y
⊢ ¬y = 1 ∧ ¬x = 1 ∧ ¬x = y

Tactic:
aesop

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Lemmas.lean
theorem isNilpotent_mulLeft_iff (a : A) : IsNilpotent (mulLeft R a) ↔ IsNilpotent a

Proof state:
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulLeft R a) ↔ IsNilpotent a

Tactic:
constructor <;> rintro ⟨n, hn⟩ <;> use n <;>
    simp only [mulLeft_eq_zero_iff, pow_mulLeft] at hn ⊢ <;>
  exact hn

Result:
no goals
-- Mathlib/Topology/MetricSpace/Dilation.lean
theorem antilipschitz : AntilipschitzWith (ratio f)⁻¹ (f : α → β) := fun x y => by
  have hr : ratio f ≠ 0 := ratio_ne_zero f
  exact mod_cast
    (ENNReal.mul_le_iff_le_inv (ENNReal.coe_ne_zero.2 hr) ENNReal.coe_ne_top).1 (edist_eq f x y).ge

Proof state:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
hr : ratio f ≠ 0
⊢ edist x y ≤ ↑(ratio f)⁻¹ * edist (f x) (f y)

Tactic:
exact mod_cast
  (ENNReal.mul_le_iff_le_inv (ENNReal.coe_ne_zero.2 hr) ENNReal.coe_ne_top).1 (edist_eq f x y).ge

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ edist x y ≤ ↑(ratio f)⁻¹ * edist (f x) (f y)

Tactic:
have hr : ratio f ≠ 0 := ratio_ne_zero f

Result:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
hr : ratio f ≠ 0
⊢ edist x y ≤ ↑(ratio f)⁻¹ * edist (f x) (f y)
-- Mathlib/Data/Option/NAry.lean
theorem map₂_eq_none_iff : map₂ f a b = none ↔ a = none ∨ b = none

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
b : Option β
⊢ map₂ f a b = none ↔ a = none ∨ b = none

Tactic:
cases a <;> cases b <;> simp

Result:
no goals
-- Mathlib/RingTheory/OreLocalization/Basic.lean
theorem smul_zero (x : R[S⁻¹]) : x • (0 : X[S⁻¹]) = 0

Proof state:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r : R
s : ↥S
⊢ (r /ₒ s) • 0 = 0

Tactic:
rw [OreLocalization.zero_def, smul_div_one, smul_zero, zero_oreDiv, zero_oreDiv]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
x : OreLocalization S R
⊢ x • 0 = 0

Tactic:
induction' x with r s

Result:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r : R
s : ↥S
⊢ (r /ₒ s) • 0 = 0
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_sin_mul_cos₂ : ∫ x in a..b, sin x * cos x = (cos a ^ 2 - cos b ^ 2) / 2

Proof state:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, sin x * cos x = (cos a ^ 2 - cos b ^ 2) / 2

Tactic:
simpa using integral_sin_pow_odd_mul_cos_pow 0 1

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem lTensor_inj_iff_rTensor_inj :
    Function.Injective (lTensor M f) ↔ Function.Injective (rTensor M f)

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
⊢ Function.Injective ⇑(lTensor M f) ↔ Function.Injective ⇑(rTensor M f)

Tactic:
simp [← comm_comp_rTensor_comp_comm_eq]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma δ_eq_δ (Q : Generators.{u₁} S T) (P : Generators.{u₂} R S)
    (P' : Generators.{u₃} R S) :
    δ Q P = δ Q P'

Proof state:
case h.mk.intro
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
P' : Generators R S
x : ↥Q.toExtension.ker
hx : Extension.Cotangent.mk x ∈ LinearMap.ker Q.toExtension.cotangentComplex
⊢ (δ Q P) ⟨Extension.Cotangent.mk x, hx⟩ = (δ Q P') ⟨Extension.Cotangent.mk x, hx⟩

Tactic:
rw [δ_eq_δAux, δ_eq_δAux]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
P' : Generators R S
⊢ δ Q P = δ Q P'

Tactic:
ext ⟨x, hx⟩

Result:
case h.mk
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
P' : Generators R S
x : Q.toExtension.Cotangent
hx : x ∈ LinearMap.ker Q.toExtension.cotangentComplex
⊢ (δ Q P) ⟨x, hx⟩ = (δ Q P') ⟨x, hx⟩

Proof state:
case h.mk
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
P' : Generators R S
x : Q.toExtension.Cotangent
hx : x ∈ LinearMap.ker Q.toExtension.cotangentComplex
⊢ (δ Q P) ⟨x, hx⟩ = (δ Q P') ⟨x, hx⟩

Tactic:
obtain ⟨x, rfl⟩ := Extension.Cotangent.mk_surjective x

Result:
case h.mk.intro
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
P' : Generators R S
x : ↥Q.toExtension.ker
hx : Extension.Cotangent.mk x ∈ LinearMap.ker Q.toExtension.cotangentComplex
⊢ (δ Q P) ⟨Extension.Cotangent.mk x, hx⟩ = (δ Q P') ⟨Extension.Cotangent.mk x, hx⟩
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem le_normalizer_of_normal [hK : (H.subgroupOf K).Normal] (HK : H ≤ K) : K ≤ H.normalizer :=
  fun x hx y =>
  ⟨fun yH => hK.conj_mem ⟨y, HK yH⟩ yH ⟨x, hx⟩, fun yH => by
    simpa [mem_subgroupOf, mul_assoc] using
      hK.conj_mem ⟨x * y * x⁻¹, HK yH⟩ yH ⟨x⁻¹, K.inv_mem hx⟩⟩

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : (H.subgroupOf K).Normal
HK : H ≤ K
x : G
hx : x ∈ K
y : G
yH : x * y * x⁻¹ ∈ H
⊢ y ∈ H

Tactic:
simpa [mem_subgroupOf, mul_assoc] using
  hK.conj_mem ⟨x * y * x⁻¹, HK yH⟩ yH ⟨x⁻¹, K.inv_mem hx⟩

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
@[to_additive]
lemma inv (h : IsUnit a) : IsUnit a⁻¹

Proof state:
case intro
α : Type u
inst✝ : DivisionMonoid α
a : α
u : αˣ
hu : ↑u = a
⊢ IsUnit a⁻¹

Tactic:
rw [← hu, ← Units.val_inv_eq_inv_val]

Result:
case intro
α : Type u
inst✝ : DivisionMonoid α
a : α
u : αˣ
hu : ↑u = a
⊢ IsUnit ↑u⁻¹

Proof state:
α : Type u
inst✝ : DivisionMonoid α
a : α
h : IsUnit a
⊢ IsUnit a⁻¹

Tactic:
obtain ⟨u, hu⟩ := h

Result:
case intro
α : Type u
inst✝ : DivisionMonoid α
a : α
u : αˣ
hu : ↑u = a
⊢ IsUnit a⁻¹

Proof state:
case intro
α : Type u
inst✝ : DivisionMonoid α
a : α
u : αˣ
hu : ↑u = a
⊢ IsUnit ↑u⁻¹

Tactic:
exact Units.isUnit _

Result:
no goals
-- Mathlib/Algebra/Order/Kleene.lean
theorem add_eq_left_iff_le : a + b = a ↔ b ≤ a

Proof state:
α : Type u_1
inst✝ : IdemSemiring α
a b : α
⊢ a + b = a ↔ b ≤ a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem perm_append_singleton (a : α) (l : List α) : l ++ [a] ~ a :: l :=
  perm_middle.trans <| by rw [append_nil]

Proof state:
α : Type u_1
a : α
l : List α
⊢ a :: (l ++ []) ~ a :: l

Tactic:
rw [append_nil]

Result:
no goals