harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean
theorem integral_comp_abs {f : ℝ → ℝ} :
    ∫ x, f |x| = 2 * ∫ x in Ioi (0 : ℝ), f x

Proof state:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x => f |x|) (Iic 0) volume
x✝ : ℝ
hx : x✝ ∈ Iic 0
⊢ x✝ ≤ 0

Tactic:
exact hx

Result:
no goals

Proof state:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
m : MeasurableEmbedding fun x => -x := Homeomorph.measurableEmbedding (Homeomorph.neg ℝ)
⊢ IntegrableOn (fun x => f |x|) (Ici 0) volume

Tactic:
exact integrableOn_Ici_iff_integrableOn_Ioi.mpr hf

Result:
no goals

Proof state:
case pos
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x => f |x|) (Iic 0) volume
⊢ ∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Ioi 0, f x

Tactic:
calc
  _ = (∫ x in Iic 0, f |x|) + ∫ x in Ioi 0, f |x| := by
    rw [← setIntegral_union (Iic_disjoint_Ioi le_rfl) measurableSet_Ioi int_Iic hf,
      Iic_union_Ioi, restrict_univ]
  _ = 2 * ∫ x in Ioi 0, f x := by
    rw [two_mul, eq]
    congr! 1
    rw [← neg_zero, ← integral_comp_neg_Iic, neg_zero]
    refine setIntegral_congr_fun measurableSet_Iic (fun _ hx => ?_)
    rw [abs_eq_neg_self.mpr (by exact hx)]

Result:
no goals

Proof state:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : Integrable (fun x => f |x|) volume
⊢ IntegrableOn (fun x => f |x|) (Ioi 0) volume

Tactic:
exact hf.integrableOn

Result:
no goals

Proof state:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
m : MeasurableEmbedding fun x => -x := Homeomorph.measurableEmbedding (Homeomorph.neg ℝ)
⊢ IntegrableOn (fun x => f |x|) (Iic 0) (Measure.map Neg.neg volume)

Tactic:
rw [m.integrableOn_map_iff]

Result:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
m : MeasurableEmbedding fun x => -x := Homeomorph.measurableEmbedding (Homeomorph.neg ℝ)
⊢ IntegrableOn ((fun x => f |x|) ∘ fun x => -x) ((fun x => -x) ⁻¹' Iic 0) volume

Proof state:
case h.e'_5
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x => f |x|) (Iic 0) volume
x✝ : ℝ
hx : x✝ ∈ Iic 0
⊢ f |x✝| = f (-x✝)

Tactic:
rw [abs_eq_neg_self.mpr (by exact hx)]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem prodMonoidal_leftUnitor_inv_snd (X : C₁ × C₂) :
    ((λ_ X).inv : X ⟶ 𝟙_ _ ⊗ X).2 = (λ_ X.2).inv

Proof state:
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
X : C₁ × C₂
⊢ (λ_ X).inv.2 = (λ_ X.2).inv

Tactic:
cases X

Result:
case mk
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (λ_ (fst✝, snd✝)).inv.2 = (λ_ (fst✝, snd✝).2).inv

Proof state:
case mk
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (λ_ (fst✝, snd✝)).inv.2 = (λ_ (fst✝, snd✝).2).inv

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Ring/NegOnePow.lean
lemma negOnePow_eq_one_iff (n : ℤ) : n.negOnePow = 1 ↔ Even n

Proof state:
case mp
n : ℤ
h : n.negOnePow = 1
⊢ ¬Odd n

Tactic:
intro h'

Result:
case mp
n : ℤ
h : n.negOnePow = 1
h' : Odd n
⊢ False

Proof state:
case mpr
n : ℤ
⊢ Even n → n.negOnePow = 1

Tactic:
exact negOnePow_even n

Result:
no goals

Proof state:
case mp
n : ℤ
⊢ n.negOnePow = 1 → Even n

Tactic:
intro h

Result:
case mp
n : ℤ
h : n.negOnePow = 1
⊢ Even n

Proof state:
case mp
n : ℤ
h : n.negOnePow = 1
⊢ Even n

Tactic:
rw [← Int.not_odd_iff_even]

Result:
case mp
n : ℤ
h : n.negOnePow = 1
⊢ ¬Odd n

Proof state:
case mp
n : ℤ
h : n.negOnePow = 1
h' : Odd n
⊢ False

Tactic:
simp only [negOnePow_odd _ h'] at h

Result:
case mp
n : ℤ
h' : Odd n
h : -1 = 1
⊢ False

Proof state:
case mp
n : ℤ
h' : Odd n
h : -1 = 1
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
n : ℤ
⊢ n.negOnePow = 1 ↔ Even n

Tactic:
constructor

Result:
case mp
n : ℤ
⊢ n.negOnePow = 1 → Even n

case mpr
n : ℤ
⊢ Even n → n.negOnePow = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_zero_right (n : Nat) : gcd n 0 = n

Proof state:
case succ
n : Nat
⊢ (0 % n.succ).gcd n.succ = n + 1

Tactic:
exact gcd_zero_left _

Result:
no goals

Proof state:
case zero

⊢ gcd 0 0 = 0

Tactic:
simp [gcd_succ]

Result:
no goals

Proof state:
n : Nat
⊢ n.gcd 0 = n

Tactic:
cases n with
| zero => simp [gcd_succ]
| succ n =>
  rw [gcd_succ]
  exact gcd_zero_left _

Result:
no goals

Proof state:
case succ
n : Nat
⊢ (n + 1).gcd 0 = n + 1

Tactic:
rw [gcd_succ]

Result:
case succ
n : Nat
⊢ (0 % n.succ).gcd n.succ = n + 1
-- Mathlib/Data/Finmap.lean
theorem ext_lookup {s₁ s₂ : Finmap β} : (∀ x, s₁.lookup x = s₂.lookup x) → s₁ = s₂ :=
  induction_on₂ s₁ s₂ fun s₁ s₂ h => by
    simp only [AList.lookup, lookup_toFinmap] at h
    rw [AList.toFinmap_eq]
    apply lookup_ext s₁.nodupKeys s₂.nodupKeys
    intro x y
    rw [h]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), lookup x ⟦s₁⟧ = lookup x ⟦s₂⟧
⊢ ⟦s₁⟧ = ⟦s₂⟧

Tactic:
simp only [AList.lookup, lookup_toFinmap] at h

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ ⟦s₁⟧ = ⟦s₂⟧

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ ∀ (x : α) (y : β x), y ∈ dlookup x s₁.entries ↔ y ∈ dlookup x s₂.entries

Tactic:
intro x y

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
x : α
y : β x
⊢ y ∈ dlookup x s₁.entries ↔ y ∈ dlookup x s₂.entries

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
x : α
y : β x
⊢ y ∈ dlookup x s₁.entries ↔ y ∈ dlookup x s₂.entries

Tactic:
rw [h]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ ⟦s₁⟧ = ⟦s₂⟧

Tactic:
rw [AList.toFinmap_eq]

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ s₁.entries ~ s₂.entries

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ s₁.entries ~ s₂.entries

Tactic:
apply lookup_ext s₁.nodupKeys s₂.nodupKeys

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ ∀ (x : α) (y : β x), y ∈ dlookup x s₁.entries ↔ y ∈ dlookup x s₂.entries
-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
theorem second_derivative_symmetric_of_eventually [IsRCLikeNormedField 𝕜]
    {f' : E → E →L[𝕜] F} {x : E}
    {f'' : E →L[𝕜] E →L[𝕜] F} (hf : ∀ᶠ y in 𝓝 x, HasFDerivAt f (f' y) y)
    (hx : HasFDerivAt f' f'' x) (v w : E) : f'' v w = f'' w v

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
x✝⁴ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝³ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x✝² : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
x✝¹ : LinearMap.CompatibleSMul E F ℝ 𝕜 := LinearMap.IsScalarTower.compatibleSMul
x✝ : LinearMap.CompatibleSMul E (E →L[𝕜] F) ℝ 𝕜 := LinearMap.IsScalarTower.compatibleSMul
f'R : E → E →L[ℝ] F := fun x => ContinuousLinearMap.restrictScalars ℝ (f' x)
hfR : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f'R y) y
f''Rl : E →ₗ[ℝ] E →ₗ[ℝ] F :=
  { toFun := fun x => { toFun := fun y => (f'' x) y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }
⊢ E →L[ℝ] E →L[ℝ] F

Tactic:
refine LinearMap.mkContinuous₂ f''Rl (‖f''‖) (fun x y ↦ ?_)

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x✝⁵ : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x✝⁵, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x✝⁵
v w : E
x✝⁴ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝³ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x✝² : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
x✝¹ : LinearMap.CompatibleSMul E F ℝ 𝕜 := LinearMap.IsScalarTower.compatibleSMul
x✝ : LinearMap.CompatibleSMul E (E →L[𝕜] F) ℝ 𝕜 := LinearMap.IsScalarTower.compatibleSMul
f'R : E → E →L[ℝ] F := fun x => ContinuousLinearMap.restrictScalars ℝ (f' x)
hfR : ∀ᶠ (y : E) in 𝓝 x✝⁵, HasFDerivAt f (f'R y) y
f''Rl : E →ₗ[ℝ] E →ₗ[ℝ] F :=
  { toFun := fun x => { toFun := fun y => (f'' x) y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }
x y : E
⊢ ‖(f''Rl x) y‖ ≤ ‖f''‖ * ‖x‖ * ‖y‖
-- Mathlib/Analysis/Complex/Hadamard.lean
/-- Another technical lemma needed in the proof. -/
private lemma bound_exp_eq {l u : ℝ} (hul : l < u) (z : ℂ) :
    (z / (↑u - ↑l)).re - ((l : ℂ) / (↑u - ↑l)).re = (z.re - l) / (u - l)

Proof state:
l u : ℝ
hul : l < u
z : ℂ
⊢ (z / (↑u - ↑l)).re - (↑l / (↑u - ↑l)).re = (z.re - l) / (u - l)

Tactic:
norm_cast

Result:
l u : ℝ
hul : l < u
z : ℂ
⊢ (z / ↑(u - l)).re - l / (u - l) = (z.re - l) / (u - l)

Proof state:
l u : ℝ
hul : l < u
z : ℂ
⊢ (z / ↑(u - l)).re - l / (u - l) = (z.re - l) / (u - l)

Tactic:
rw [Complex.div_re, Complex.normSq_ofReal, Complex.ofReal_re, Complex.ofReal_im, mul_div_assoc,
  div_mul_eq_div_div_swap, div_self (by norm_cast; linarith),
  ← div_eq_mul_one_div]

Result:
l u : ℝ
hul : l < u
z : ℂ
⊢ z.re / (u - l) + z.im * 0 / ((u - l) * (u - l)) - l / (u - l) = (z.re - l) / (u - l)

Proof state:
l u : ℝ
hul : l < u
z : ℂ
⊢ z.re / (u - l) - l / (u - l) = (z.re - l) / (u - l)

Tactic:
rw [← div_sub_div_same]

Result:
no goals

Proof state:
l u : ℝ
hul : l < u
z : ℂ
⊢ z.re / (u - l) + z.im * 0 / ((u - l) * (u - l)) - l / (u - l) = (z.re - l) / (u - l)

Tactic:
simp only [mul_zero, zero_div, add_zero]

Result:
l u : ℝ
hul : l < u
z : ℂ
⊢ z.re / (u - l) - l / (u - l) = (z.re - l) / (u - l)

Proof state:
l u : ℝ
hul : l < u
z : ℂ
⊢ ¬u - l = 0

Tactic:
linarith

Result:
no goals

Proof state:
l u : ℝ
hul : l < u
z : ℂ
⊢ u - l ≠ 0

Tactic:
norm_cast

Result:
l u : ℝ
hul : l < u
z : ℂ
⊢ ¬u - l = 0
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem coe_bot : (⊥ : YoungDiagram) = (∅ : Set (ℕ × ℕ))

Proof state:
⊢ ↑⊥ = ∅

Tactic:
ext

Result:
case h
x✝ : ℕ × ℕ
⊢ x✝ ∈ ↑⊥ ↔ x✝ ∈ ∅

Proof state:
case h
x✝ : ℕ × ℕ
⊢ x✝ ∈ ↑⊥ ↔ x✝ ∈ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Control/Basic.lean
theorem CommApplicative.commutative_map {m : Type u → Type v} [h : Applicative m]
    [CommApplicative m] {α β γ} (a : m α) (b : m β) {f : α → β → γ} :
  f <$> a <*> b = flip f <$> b <*> a :=
  calc
    f <$> a <*> b = (fun p : α × β => f p.1 p.2) <$> (Prod.mk <$> a <*> b)

Proof state:
m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ f <$> a <*> b = (fun p => f p.fst p.snd) <$> (Prod.mk <$> a <*> b)

Tactic:
simp only [map_seq, map_map, Function.comp_def]

Result:
no goals

Proof state:
m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (fun p => f p.fst p.snd) <$> (Prod.mk <$> a <*> b) = (fun b a => f a b) <$> b <*> a

Tactic:
rw [@CommApplicative.commutative_prod m h]

Result:
m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (fun p => f p.fst p.snd) <$> ((fun b a => (a, b)) <$> b <*> a) = (fun b a => f a b) <$> b <*> a

Proof state:
m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (fun a => (fun p => f p.fst p.snd) ∘ fun a_1 => (a_1, a)) <$> b <*> a = (fun b a => f a b) <$> b <*> a

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem factorial_lt (hn : 0 < n) : n ! < m ! ↔ n < m

Proof state:
m n : ℕ
hn : 0 < n
h : n < m
⊢ n ! < m !

Tactic:
have : ∀ {n}, 0 < n → n ! < (n + 1)! := by
  intro k hk
  rw [factorial_succ, succ_mul, Nat.lt_add_left_iff_pos]
  exact Nat.mul_pos hk k.factorial_pos

Result:
m n : ℕ
hn : 0 < n
h : n < m
this : ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!
⊢ n ! < m !

Proof state:
case step
m n : ℕ
this : ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!
m✝ : ℕ
hnk : n.succ.le m✝
ih : 0 < n → n ! < m✝!
hn : 0 < n
⊢ n ! < m✝.succ !

Tactic:
exact lt_trans (ih hn) <| this <| lt_trans hn <| lt_of_succ_le hnk

Result:
no goals

Proof state:
m n : ℕ
hn : 0 < n
h : n < m
this : ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!
⊢ n ! < m !

Tactic:
induction h generalizing hn with
| refl => exact this hn
| step hnk ih => exact lt_trans (ih hn) <| this <| lt_trans hn <| lt_of_succ_le hnk

Result:
no goals

Proof state:
case refl
m n : ℕ
this : ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!
hn : 0 < n
⊢ n ! < n.succ !

Tactic:
exact this hn

Result:
no goals

Proof state:
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ 0 < k * k !

Tactic:
exact Nat.mul_pos hk k.factorial_pos

Result:
no goals

Proof state:
m n : ℕ
hn : 0 < n
⊢ n ! < m ! ↔ n < m

Tactic:
refine ⟨fun h => not_le.mp fun hmn => Nat.not_le_of_lt h (factorial_le hmn), fun h => ?_⟩

Result:
m n : ℕ
hn : 0 < n
h : n < m
⊢ n ! < m !

Proof state:
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ k ! < (k + 1)!

Tactic:
rw [factorial_succ, succ_mul, Nat.lt_add_left_iff_pos]

Result:
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ 0 < k * k !

Proof state:
m n : ℕ
hn : 0 < n
h : n < m
⊢ ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!

Tactic:
intro k hk

Result:
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ k ! < (k + 1)!
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem Function.Injective.lieAlgebra_isNilpotent [h₁ : IsNilpotent L'] {f : L →ₗ⁅R⁆ L'}
    (h₂ : Function.Injective f) : IsNilpotent L

Proof state:
case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : ∃ k, lowerCentralSeries R L' L' k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Injective ⇑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ lowerCentralSeries R L L k = ⊥

Tactic:
apply LieIdeal.bot_of_map_eq_bot h₂

Result:
case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : ∃ k, lowerCentralSeries R L' L' k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Injective ⇑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ LieIdeal.map f (lowerCentralSeries R L L k) = ⊥

Proof state:
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieRing.IsNilpotent L'
f : L →ₗ⁅R⁆ L'
h₂ : Injective ⇑f
⊢ LieRing.IsNilpotent L

Tactic:
rw [LieRing.IsNilpotent, LieModule.isNilpotent_iff R] at h₁ ⊢

Result:
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : ∃ k, lowerCentralSeries R L' L' k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Injective ⇑f
⊢ ∃ k, lowerCentralSeries R L L k = ⊥

Proof state:
case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : ∃ k, lowerCentralSeries R L' L' k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Injective ⇑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ LieIdeal.map f (lowerCentralSeries R L L k) = ⊥

Tactic:
rw [eq_bot_iff, ← hk]

Result:
case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : ∃ k, lowerCentralSeries R L' L' k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Injective ⇑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ LieIdeal.map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k

Proof state:
case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : ∃ k, lowerCentralSeries R L' L' k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Injective ⇑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ LieIdeal.map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k

Tactic:
apply LieIdeal.map_lowerCentralSeries_le

Result:
no goals

Proof state:
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : ∃ k, lowerCentralSeries R L' L' k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Injective ⇑f
⊢ ∃ k, lowerCentralSeries R L L k = ⊥

Tactic:
peel h₁ with k hk

Result:
case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : ∃ k, lowerCentralSeries R L' L' k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Injective ⇑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ lowerCentralSeries R L L k = ⊥
-- Mathlib/CategoryTheory/Iso.lean
theorem of_isIso_fac_right {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [IsIso g]
    [hh : IsIso h] (w : f ≫ g = h) : IsIso f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso g
hh : IsIso h
w : f ≫ g = h
⊢ IsIso f

Tactic:
rw [← w] at hh

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso g
hh : IsIso (f ≫ g)
w : f ≫ g = h
⊢ IsIso f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso g
hh : IsIso (f ≫ g)
w : f ≫ g = h
⊢ IsIso f

Tactic:
haveI := hh

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso g
hh : IsIso (f ≫ g)
w : f ≫ g = h
this : IsIso (f ≫ g)
⊢ IsIso f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso g
hh : IsIso (f ≫ g)
w : f ≫ g = h
this : IsIso (f ≫ g)
⊢ IsIso f

Tactic:
exact of_isIso_comp_right f g

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
theorem Ideal.IsHomogeneous.iff_exists :
    I.IsHomogeneous 𝒜 ↔ ∃ S : Set (homogeneousSubmonoid 𝒜), I = Ideal.span ((↑) '' S)

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ IsHomogeneous 𝒜 I ↔ ∃ S, I = span (Subtype.val '' S)

Tactic:
rw [Ideal.IsHomogeneous.iff_eq, eq_comm]

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ I = (homogeneousCore 𝒜 I).toIdeal ↔ ∃ S, I = span (Subtype.val '' S)

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ I = (homogeneousCore 𝒜 I).toIdeal ↔ ∃ S, I = span (Subtype.val '' S)

Tactic:
exact ((Set.image_preimage.compose (Submodule.gi _ _).gc).exists_eq_l _).symm

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_inter_preimage (f : α → β) (s : Set α) (t : Set β) :
    f '' (s ∩ f ⁻¹' t) = f '' s ∩ t

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' (s ∩ f ⁻¹' t) = f '' s ∩ t

Tactic:
apply Subset.antisymm

Result:
case h₁
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' (s ∩ f ⁻¹' t) ⊆ f '' s ∩ t

case h₂
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' s ∩ t ⊆ f '' (s ∩ f ⁻¹' t)

Proof state:
case h₂.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
h' : x ∈ s
h : f x ∈ t
⊢ f x ∈ f '' (s ∩ f ⁻¹' t)

Tactic:
exact ⟨x, ⟨h', h⟩, rfl⟩

Result:
no goals

Proof state:
case h₁
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' (s ∩ f ⁻¹' t) ⊆ f '' s ∩ t

Tactic:
calc
  f '' (s ∩ f ⁻¹' t) ⊆ f '' s ∩ f '' (f ⁻¹' t) := image_inter_subset _ _ _
  _ ⊆ f '' s ∩ t := inter_subset_inter_right _ (image_preimage_subset f t)

Result:
no goals

Proof state:
case h₂
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' s ∩ t ⊆ f '' (s ∩ f ⁻¹' t)

Tactic:
rintro _ ⟨⟨x, h', rfl⟩, h⟩

Result:
case h₂.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
h' : x ∈ s
h : f x ∈ t
⊢ f x ∈ f '' (s ∩ f ⁻¹' t)
-- Mathlib/Data/Bool/Basic.lean
theorem ofNat_toNat (b : Bool) : ofNat (toNat b) = b

Proof state:
b : Bool
⊢ ofNat b.toNat = b

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/IntegralRNDeriv.lean
/-- For a convex continuous function `f` on `[0, ∞)`, if `μ` is absolutely continuous
with respect to a probability measure `ν`, then
`f (μ univ).toReal ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν`. -/
lemma le_integral_rnDeriv_of_ac [IsFiniteMeasure μ] [IsProbabilityMeasure ν]
    (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousWithinAt f (Ici 0) 0)
    (hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν) (hμν : μ ≪ ν) :
    f (μ univ).toReal ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν

Proof state:
case inr
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
x : ℝ
hx : x ∈ Ici 0
hx_pos : 0 < x
h : x ∈ interior (Ici 0) → ContinuousWithinAt f (interior (Ici 0)) x
⊢ ContinuousWithinAt f (Ici 0) x

Tactic:
simp only [nonempty_Iio, interior_Ici', mem_Ioi] at h

Result:
case inr
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
x : ℝ
hx : x ∈ Ici 0
hx_pos : 0 < x
h : 0 < x → ContinuousWithinAt f (Ioi 0) x
⊢ ContinuousWithinAt f (Ici 0) x