harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToSimpleFunc_smul_left' (T T' : Set α → E →L[ℝ] F') (c : ℝ)
    (h_smul : ∀ s, MeasurableSet s → μ s < ∞ → T' s = c • T s) {f : α →ₛ E} (hf : Integrable f μ) :
    setToSimpleFunc T' f = c • setToSimpleFunc T f

Proof state:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable (⇑f) μ
this : ∀ x ∈ filter (fun x => x ≠ 0) f.range, T' (⇑f ⁻¹' {x}) = c • T (⇑f ⁻¹' {x})
⊢ ∑ x ∈ filter (fun x => x ≠ 0) f.range, (T' (⇑f ⁻¹' {x})) x =
    ∑ x ∈ filter (fun x => x ≠ 0) f.range, c • (T (⇑f ⁻¹' {x})) x

Tactic:
refine Finset.sum_congr rfl fun x hx => ?_

Result:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable (⇑f) μ
this : ∀ x ∈ filter (fun x => x ≠ 0) f.range, T' (⇑f ⁻¹' {x}) = c • T (⇑f ⁻¹' {x})
x : E
hx : x ∈ filter (fun x => x ≠ 0) f.range
⊢ (T' (⇑f ⁻¹' {x})) x = c • (T (⇑f ⁻¹' {x})) x

Proof state:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable (⇑f) μ
x : E
hx : x ∈ filter (fun x => x ≠ 0) f.range
⊢ x ≠ 0

Tactic:
rw [mem_filter] at hx

Result:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable (⇑f) μ
x : E
hx : x ∈ f.range ∧ x ≠ 0
⊢ x ≠ 0

Proof state:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable (⇑f) μ
x : E
hx : x ∈ filter (fun x => x ≠ 0) f.range
⊢ T' (⇑f ⁻¹' {x}) = c • T (⇑f ⁻¹' {x})

Tactic:
refine
  h_smul (f ⁻¹' {x}) (measurableSet_preimage _ _) (measure_preimage_lt_top_of_integrable _ hf ?_)

Result:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable (⇑f) μ
x : E
hx : x ∈ filter (fun x => x ≠ 0) f.range
⊢ x ≠ 0
-- Mathlib/Analysis/RCLike/Basic.lean
protected lemma inv_pos_of_pos (hz : 0 < z) : 0 < z⁻¹

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
hz : 0 < z
⊢ 0 < z⁻¹

Tactic:
rw [pos_iff_exists_ofReal] at hz

Result:
K : Type u_1
inst✝ : RCLike K
z : K
hz : ∃ x > 0, ↑x = z
⊢ 0 < z⁻¹

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
hz : ∃ x > 0, ↑x = z
⊢ 0 < z⁻¹

Tactic:
obtain ⟨x, hx, hx'⟩ := hz

Result:
case intro.intro
K : Type u_1
inst✝ : RCLike K
z : K
x : ℝ
hx : x > 0
hx' : ↑x = z
⊢ 0 < z⁻¹

Proof state:
case intro.intro
K : Type u_1
inst✝ : RCLike K
z : K
x : ℝ
hx : x > 0
hx' : ↑x = z
⊢ 0 < x⁻¹

Tactic:
exact inv_pos_of_pos hx

Result:
no goals

Proof state:
case intro.intro
K : Type u_1
inst✝ : RCLike K
z : K
x : ℝ
hx : x > 0
hx' : ↑x = z
⊢ 0 < z⁻¹

Tactic:
rw [← hx', ← ofReal_inv, ofReal_pos]

Result:
case intro.intro
K : Type u_1
inst✝ : RCLike K
z : K
x : ℝ
hx : x > 0
hx' : ↑x = z
⊢ 0 < x⁻¹
-- Mathlib/Analysis/Convex/Function.lean
theorem StrictConcaveOn.congr (hf : StrictConcaveOn 𝕜 s f) (hfg : EqOn f g s) :
    StrictConcaveOn 𝕜 s g :=
  ⟨hf.1, fun x hx y hy hxy a b ha hb hab => by
    simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha.le hb.le hab)] using
      hf.2 hx hy hxy ha hb hab⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f g : E → β
hf : StrictConcaveOn 𝕜 s f
hfg : EqOn f g s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • g x + b • g y < g (a • x + b • y)

Tactic:
simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha.le hb.le hab)] using
  hf.2 hx hy hxy ha hb hab

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem exists_range_iff {f : α →ₛ β} {p : β → Prop} : (∃ y ∈ f.range, p y) ↔ ∃ x, p (f x)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f : α →ₛ β
p : β → Prop
⊢ (∃ y ∈ f.range, p y) ↔ ∃ x, p (f x)

Tactic:
simpa only [mem_range, exists_prop] using Set.exists_range_iff

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Content.lean
theorem is_mul_left_invariant_innerContent [Group G] [IsTopologicalGroup G]
    (h : ∀ (g : G) {K : Compacts G}, μ (K.map _ <| continuous_mul_left g) = μ K) (g : G)
    (U : Opens G) :
    μ.innerContent (Opens.comap (Homeomorph.mulLeft g) U) = μ.innerContent U

Proof state:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun b => g * b) ⋯ K) = μ K
g : G
U : Opens G
⊢ μ.innerContent ((Opens.comap ↑(Homeomorph.mulLeft g)) U) = μ.innerContent U

Tactic:
convert μ.innerContent_comap (Homeomorph.mulLeft g) (fun K => h g) U

Result:
no goals
-- Mathlib/Algebra/Lie/Solvable.lean
theorem derivedSeriesOfIdeal_add_le_add (J : LieIdeal R L) (k l : ℕ) :
    D (k + l) (I + J) ≤ D k I + D l J

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L := { toFun := fun I => ⁅I, I⁆, monotone' := ⋯ }
⊢ D (k + l) (I + J) ≤ D k I + D l J

Tactic:
have h₁ : ∀ I J : LieIdeal R L, D₁ (I ⊔ J) ≤ D₁ I ⊔ J := by
  simp [D₁, LieSubmodule.lie_le_right, LieSubmodule.lie_le_left, le_sup_of_le_right]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L := { toFun := fun I => ⁅I, I⁆, monotone' := ⋯ }
h₁ : ∀ (I J : LieIdeal R L), D₁ (I ⊔ J) ≤ D₁ I ⊔ J
⊢ D (k + l) (I + J) ≤ D k I + D l J

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
k l : ℕ
⊢ D (k + l) (I + J) ≤ D k I + D l J

Tactic:
let D₁ : LieIdeal R L →o LieIdeal R L :=
  { toFun := fun I => ⁅I, I⁆
    monotone' := fun I J h => LieSubmodule.mono_lie h h }

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L := { toFun := fun I => ⁅I, I⁆, monotone' := ⋯ }
⊢ D (k + l) (I + J) ≤ D k I + D l J

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L := { toFun := fun I => ⁅I, I⁆, monotone' := ⋯ }
⊢ ∀ (I J : LieIdeal R L), D₁ (I ⊔ J) ≤ D₁ I ⊔ J

Tactic:
simp [D₁, LieSubmodule.lie_le_right, LieSubmodule.lie_le_left, le_sup_of_le_right]

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L := { toFun := fun I => ⁅I, I⁆, monotone' := ⋯ }
h₁ : ∀ (I J : LieIdeal R L), D₁ (I ⊔ J) ≤ D₁ I ⊔ J
⊢ D (k + l) (I + J) ≤ D k I + D l J

Tactic:
rw [← D₁.iterate_sup_le_sup_iff] at h₁

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L := { toFun := fun I => ⁅I, I⁆, monotone' := ⋯ }
h₁ : ∀ (n₁ n₂ : ℕ) (a₁ a₂ : LieIdeal R L), (⇑D₁)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑D₁)^[n₁] a₁ ⊔ (⇑D₁)^[n₂] a₂
⊢ D (k + l) (I + J) ≤ D k I + D l J

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L := { toFun := fun I => ⁅I, I⁆, monotone' := ⋯ }
h₁ : ∀ (n₁ n₂ : ℕ) (a₁ a₂ : LieIdeal R L), (⇑D₁)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑D₁)^[n₁] a₁ ⊔ (⇑D₁)^[n₂] a₂
⊢ D (k + l) (I + J) ≤ D k I + D l J

Tactic:
exact h₁ k l I J

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean
@[reassoc (attr := simp)]
lemma inr_f_descShortComplex_f (n : ℤ) : (inr S.f).f n ≫ (descShortComplex S).f n = S.g.f n

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
n : ℤ
⊢ (inr S.f).f n ≫ (descShortComplex S).f n = S.g.f n

Tactic:
simp [descShortComplex]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem dualMap_injective_iff {f : V₁ →ₗ[K] V₂} :
    Function.Injective f.dualMap ↔ Function.Surjective f

Proof state:
K : Type uK
inst✝⁴ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ Function.Injective ⇑f.dualMap ↔ Function.Surjective ⇑f

Tactic:
refine ⟨Function.mtr fun not_surj inj ↦ ?_, dualMap_injective_of_surjective⟩

Result:
K : Type uK
inst✝⁴ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
not_surj : ¬Function.Surjective ⇑f
inj : Function.Injective ⇑f.dualMap
⊢ False

Proof state:
K : Type uK
inst✝⁴ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
not_surj : ¬Function.Surjective ⇑f
inj : Function.Injective ⇑f.dualMap
⊢ False

Tactic:
rw [← range_eq_top, ← Ne, ← lt_top_iff_ne_top] at not_surj

Result:
K : Type uK
inst✝⁴ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
not_surj : range f < ⊤
inj : Function.Injective ⇑f.dualMap
⊢ False

Proof state:
case intro.intro
K : Type uK
inst✝⁴ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
not_surj : range f < ⊤
inj : Function.Injective ⇑f.dualMap
φ : V₂ →ₗ[K] K
φ0 : φ ≠ 0
range_le_ker : range f ≤ ker φ
⊢ False

Tactic:
exact φ0 (inj <| ext fun x ↦ range_le_ker ⟨x, rfl⟩)

Result:
no goals

Proof state:
K : Type uK
inst✝⁴ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
not_surj : range f < ⊤
inj : Function.Injective ⇑f.dualMap
⊢ False

Tactic:
obtain ⟨φ, φ0, range_le_ker⟩ := (range f).exists_le_ker_of_lt_top not_surj

Result:
case intro.intro
K : Type uK
inst✝⁴ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
not_surj : range f < ⊤
inj : Function.Injective ⇑f.dualMap
φ : V₂ →ₗ[K] K
φ0 : φ ≠ 0
range_le_ker : range f ≤ ker φ
⊢ False
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem isCycleOn_singleton : f.IsCycleOn {a} ↔ f a = a

Proof state:
α : Type u_2
f : Perm α
a : α
⊢ f.IsCycleOn {a} ↔ f a = a

Tactic:
simp [IsCycleOn, SameCycle.rfl]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem piPremeasure_pi_eval {s : Set (∀ i, α i)} :
    piPremeasure m (pi univ fun i => eval i '' s) = piPremeasure m s

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : Set ((i : ι) → α i)
⊢ piPremeasure m (univ.pi fun i => eval i '' s) = piPremeasure m s

Tactic:
simp only [eval, piPremeasure_pi']

Result:
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : Set ((i : ι) → α i)
⊢ ∏ i : ι, (m i) ((fun a => a i) '' s) = piPremeasure m s

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : Set ((i : ι) → α i)
⊢ ∏ i : ι, (m i) ((fun a => a i) '' s) = piPremeasure m s

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem inf_iInf [Nonempty ι] {f : ι → α} {a : α} : (a ⊓ ⨅ x, f x) = ⨅ x, a ⊓ f x

Proof state:
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ a ⊓ ⨅ x, f x = ⨅ x, a ⊓ f x

Tactic:
rw [iInf_inf_eq, iInf_const]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem det_matrixOfPolynomials {n : ℕ} (p : Fin n → R[X])
    (h_deg : ∀ i, (p i).natDegree = i) (h_monic : ∀ i, Monic <| p i) :
    (Matrix.of (fun (i j : Fin n) => (p j).coeff i)).det = 1

Proof state:
case h.e'_2.a
R : Type v
inst✝ : CommRing R
n : ℕ
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree = ↑i
h_monic : ∀ (i : Fin n), (p i).Monic
x : Fin n
a✝ : x ∈ univ
⊢ of (fun i j => (p j).coeff ↑i) x x = 1

Tactic:
rw [Matrix.of_apply, ← h_deg, coeff_natDegree, (h_monic x).leadingCoeff]

Result:
no goals

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree = ↑i
h_monic : ∀ (i : Fin n), (p i).Monic
⊢ ∏ i : Fin n, of (fun i j => (p j).coeff ↑i) i i = 1

Tactic:
convert prod_const_one with x _

Result:
case h.e'_2.a
R : Type v
inst✝ : CommRing R
n : ℕ
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree = ↑i
h_monic : ∀ (i : Fin n), (p i).Monic
x : Fin n
a✝ : x ∈ univ
⊢ of (fun i j => (p j).coeff ↑i) x x = 1

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree = ↑i
h_monic : ∀ (i : Fin n), (p i).Monic
⊢ (of fun i j => (p j).coeff ↑i).det = 1

Tactic:
rw [Matrix.det_of_upperTriangular (Matrix.matrixOfPolynomials_blockTriangular p (fun i ↦
    Nat.le_of_eq (h_deg i)))]

Result:
R : Type v
inst✝ : CommRing R
n : ℕ
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree = ↑i
h_monic : ∀ (i : Fin n), (p i).Monic
⊢ ∏ i : Fin n, of (fun i j => (p j).coeff ↑i) i i = 1
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sup_typein_succ {o : Ordinal} :
    sup.{u, u} (typein ((· < ·) : (succ o).toType → (succ o).toType → Prop)) = o

Proof state:
case inr
o : Ordinal.{u}
h : succ (sup ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding) = lsub ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding
⊢ sup ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding = o

Tactic:
rw [← succ_eq_succ_iff, h]

Result:
case inr
o : Ordinal.{u}
h : succ (sup ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding) = lsub ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding
⊢ lsub ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding = succ o

Proof state:
case inl
o : Ordinal.{u}
h : sup ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding = lsub ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding
⊢ sup ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding = o

Tactic:
rw [sup_eq_lsub_iff_succ] at h

Result:
case inl
o : Ordinal.{u}
h :
  ∀ a < lsub ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding, succ a < lsub ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding
⊢ sup ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding = o

Proof state:
case inl
o : Ordinal.{u}
h :
  ∀ a < lsub ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding, succ a < lsub ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding
⊢ sup ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding = o

Tactic:
simp only [lsub_typein] at h

Result:
case inl
o : Ordinal.{u}
h : ∀ a < succ o, succ a < succ o
⊢ sup ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding = o

Proof state:
case inr
o : Ordinal.{u}
h : succ (sup ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding) = lsub ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding
⊢ lsub ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding = succ o

Tactic:
apply lsub_typein

Result:
no goals

Proof state:
case inl
o : Ordinal.{u}
h : ∀ a < succ o, succ a < succ o
⊢ sup ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding = o

Tactic:
exact (h o (lt_succ o)).false.elim

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/Basic.lean
@[simp] lemma map_add_right_Icc (a b c : α) :
    (Icc a b).map (addRightEmbedding c) = Icc (a + c) (b + c)

Proof state:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addRightEmbedding c) '' Set.Icc a b = Set.Icc (a + c) (b + c)

Tactic:
exact Set.image_add_const_Icc _ _ _

Result:
no goals

Proof state:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addRightEmbedding c) (Icc a b) = Icc (a + c) (b + c)

Tactic:
rw [← coe_inj, coe_map, coe_Icc, coe_Icc]

Result:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addRightEmbedding c) '' Set.Icc a b = Set.Icc (a + c) (b + c)
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
theorem mapOfMeasurable_eq_map (κ : Kernel α β) {f : β → γ} (hf : Measurable f) :
    mapOfMeasurable κ f hf = map κ f

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
f : β → γ
hf : Measurable f
⊢ κ.mapOfMeasurable f hf = κ.map f

Tactic:
simp [map, hf]

Result:
no goals
-- Mathlib/Algebra/Tropical/BigOperators.lean
theorem Finset.trop_inf [LinearOrder R] [OrderTop R] (s : Finset S) (f : S → R) :
    trop (s.inf f) = ∑ i ∈ s, trop (f i)

Proof state:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ ∑ i ∈ s, trop (f i) = (Multiset.map (fun i => trop (f i)) s.val).sum

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ ∑ i ∈ s, trop (f i) = (Multiset.map trop (Multiset.map f s.val)).sum

Tactic:
simp only [Multiset.map_map, Function.comp_apply]

Result:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ ∑ i ∈ s, trop (f i) = (Multiset.map (fun i => trop (f i)) s.val).sum

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ trop (s.inf f) = ∑ i ∈ s, trop (f i)

Tactic:
convert Multiset.trop_inf (s.val.map f)

Result:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ ∑ i ∈ s, trop (f i) = (Multiset.map trop (Multiset.map f s.val)).sum
-- Mathlib/Topology/UniformSpace/Pi.lean
lemma Pi.uniformSpace_comap_restrict_sUnion (𝔖 : Set (Set ι)) :
    UniformSpace.comap (⋃₀ 𝔖).restrict (Pi.uniformSpace (fun i : (⋃₀ 𝔖) ↦ α i)) =
    ⨅ S ∈ 𝔖, UniformSpace.comap S.restrict (Pi.uniformSpace (fun i : S ↦ α i))

Proof state:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
𝔖 : Set (Set ι)
⊢ UniformSpace.comap (⋃₀ 𝔖).restrict (uniformSpace fun i => α ↑i) =
    ⨅ S ∈ 𝔖, UniformSpace.comap S.restrict (uniformSpace fun i => α ↑i)

Tactic:
simp_rw [Pi.uniformSpace_comap_restrict α, iInf_sUnion]

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem lt_factorial_self {n : ℕ} (hi : 3 ≤ n) : n < n !

Proof state:
n : ℕ
hi : 3 ≤ n
this : 0 < n
hn : 1 < n.pred
⊢ n.pred.succ < (n.pred + 1) * n.pred !

Tactic:
exact (Nat.lt_mul_iff_one_lt_right (pred n).succ_pos).2
  ((Nat.lt_of_lt_of_le hn (self_le_factorial _)))

Result:
no goals

Proof state:
n : ℕ
hi : 3 ≤ n
⊢ 0 < n

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
hi : 3 ≤ n
this : 0 < n
hn : 1 < n.pred
⊢ n < n !

Tactic:
rw [← succ_pred_eq_of_pos ‹0 < n›, factorial_succ]

Result:
n : ℕ
hi : 3 ≤ n
this : 0 < n
hn : 1 < n.pred
⊢ n.pred.succ < (n.pred + 1) * n.pred !

Proof state:
n : ℕ
hi : 3 ≤ n
⊢ n < n !

Tactic:
have : 0 < n := by omega

Result:
n : ℕ
hi : 3 ≤ n
this : 0 < n
⊢ n < n !

Proof state:
n : ℕ
hi : 3 ≤ n
this : 0 < n
⊢ n < n !

Tactic:
have hn : 1 < pred n := le_pred_of_lt (succ_le_iff.mp hi)

Result:
n : ℕ
hi : 3 ≤ n
this : 0 < n
hn : 1 < n.pred
⊢ n < n !
-- Mathlib/Algebra/FreeMonoid/Basic.lean
theorem toList_prod (xs : List (FreeMonoid α)) : toList xs.prod = (xs.map toList).flatten

Proof state:
α : Type u_1
xs : List (FreeMonoid α)
⊢ toList xs.prod = (List.map (⇑toList) xs).flatten

Tactic:
induction xs <;> simp [*, List.flatten]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Prod.lean
theorem sup'_inf_sup' (f : ι → α) (g : κ → α) :
    s.sup' hs f ⊓ t.sup' ht g = (s ×ˢ t).sup' (hs.product ht) fun i => f i.1 ⊓ g i.2

Proof state:
α : Type u_2
ι : Type u_5
κ : Type u_6
inst✝ : DistribLattice α
s : Finset ι
t : Finset κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → α
g : κ → α
⊢ s.sup' hs f ⊓ t.sup' ht g = (s ×ˢ t).sup' ⋯ fun i => f i.1 ⊓ g i.2

Tactic:
simp_rw [Finset.sup'_inf_distrib_right, Finset.sup'_inf_distrib_left, sup'_product_left]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem Filter.EventuallyLE.prodMap_nhds {α β : Type*} [LE α] [LE β] {f₁ f₂ : X → α} {g₁ g₂ : Y → β}
    {x : X} {y : Y} (hf : f₁ ≤ᶠ[𝓝 x] f₂) (hg : g₁ ≤ᶠ[𝓝 y] g₂) :
    Prod.map f₁ g₁ ≤ᶠ[𝓝 (x, y)] Prod.map f₂ g₂

Proof state:
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ ≤ᶠ[𝓝 x] f₂
hg : g₁ ≤ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ ≤ᶠ[𝓝 (x, y)] Prod.map f₂ g₂

Tactic:
rw [nhds_prod_eq]

Result:
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ ≤ᶠ[𝓝 x] f₂
hg : g₁ ≤ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ ≤ᶠ[𝓝 x ×ˢ 𝓝 y] Prod.map f₂ g₂

Proof state:
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ ≤ᶠ[𝓝 x] f₂
hg : g₁ ≤ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ ≤ᶠ[𝓝 x ×ˢ 𝓝 y] Prod.map f₂ g₂

Tactic:
exact hf.prod_map hg

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem mul_eq_one_iff : s * t = 1 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
⊢ s * t = 1 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
simp_rw [← coe_inj, coe_mul, coe_one, Set.mul_eq_one_iff, coe_singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapFinIdx_ne_empty_iff {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} :
    l.mapFinIdx f ≠ #[] ↔ l ≠ #[]

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : (i : Nat) → α → i < l.size → β
⊢ l.mapFinIdx f ≠ #[] ↔ l ≠ #[]

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Basic.lean
theorem IsNilpotent.neg [Ring R] (h : IsNilpotent x) : IsNilpotent (-x)

Proof state:
case intro
R : Type u_1
x : R
inst✝ : Ring R
n : ℕ
hn : x ^ n = 0
⊢ IsNilpotent (-x)

Tactic:
use n

Result:
case h
R : Type u_1
x : R
inst✝ : Ring R
n : ℕ
hn : x ^ n = 0
⊢ (-x) ^ n = 0

Proof state:
case h
R : Type u_1
x : R
inst✝ : Ring R
n : ℕ
hn : x ^ n = 0
⊢ (-x) ^ n = 0

Tactic:
rw [neg_pow, hn, mul_zero]

Result:
no goals

Proof state:
R : Type u_1
x : R
inst✝ : Ring R
h : IsNilpotent x
⊢ IsNilpotent (-x)

Tactic:
obtain ⟨n, hn⟩ := h

Result:
case intro
R : Type u_1
x : R
inst✝ : Ring R
n : ℕ
hn : x ^ n = 0
⊢ IsNilpotent (-x)
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem continuous_exp : Continuous exp :=
  continuous_iff_continuousAt.mpr fun x =>
    continuousAt_of_locally_lipschitz zero_lt_one (2 * ‖exp x‖)
      (fun y ↦ by
        convert locally_lipschitz_exp zero_le_one le_rfl x y using 2
        congr
        ring)

Proof state:
case h'.h.e'_4.e_a.e_a
x y : ℂ
a✝ : ‖y - x‖ < 1
⊢ 2 = 1 + 1

Tactic:
ring

Result:
no goals

Proof state:
x y : ℂ
⊢ dist y x < 1 → dist (cexp y) (cexp x) ≤ 2 * ‖cexp x‖ * dist y x

Tactic:
convert locally_lipschitz_exp zero_le_one le_rfl x y using 2

Result:
case h'.h.e'_4
x y : ℂ
a✝ : ‖y - x‖ < 1
⊢ 2 * ‖cexp x‖ * dist y x = (1 + 1) * ‖cexp x‖ * ‖y - x‖

Proof state:
case h'.h.e'_4
x y : ℂ
a✝ : ‖y - x‖ < 1
⊢ 2 * ‖cexp x‖ * dist y x = (1 + 1) * ‖cexp x‖ * ‖y - x‖

Tactic:
congr

Result:
case h'.h.e'_4.e_a.e_a
x y : ℂ
a✝ : ‖y - x‖ < 1
⊢ 2 = 1 + 1