harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
lemma degreeOf_le_iff {n : σ} {f : MvPolynomial σ R} {d : ℕ} :
    degreeOf n f ≤ d ↔ ∀ m ∈ support f, m n ≤ d

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
d : ℕ
⊢ degreeOf n f ≤ d ↔ ∀ m ∈ f.support, m n ≤ d

Tactic:
rw [degreeOf_eq_sup, Finset.sup_le_iff]

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Isometry.lean
theorem dist_pointReflection_fixed (x y : P) : dist (pointReflection 𝕜 x y) x = dist y x

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
x y : P
⊢ dist ((pointReflection 𝕜 x) y) x = dist y x

Tactic:
rw [← (pointReflection 𝕜 x).dist_map y x, pointReflection_self]

Result:
no goals
-- Mathlib/Data/Nat/Find.lean
@[simp] lemma le_find_iff (h : ∃ n : ℕ, p n) (n : ℕ) : n ≤ Nat.find h ↔ ∀ m < n, ¬ p m

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ
⊢ n ≤ Nat.find h ↔ ∀ (m : ℕ), m < n → ¬p m

Tactic:
simp only [← not_lt, find_lt_iff, not_exists, not_and]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem zero_rpow_mul_self (y : ℝ) : (0 : ℝ≥0∞) ^ y * (0 : ℝ≥0∞) ^ y = (0 : ℝ≥0∞) ^ y

Proof state:
case pos
y : ℝ
h✝ : 0 < y
⊢ 0 * 0 = 0

case pos
y : ℝ
h✝¹ : ¬0 < y
h✝ : y = 0
⊢ 1 * 1 = 1

case neg
y : ℝ
h✝¹ : ¬0 < y
h✝ : ¬y = 0
⊢ ⊤ * ⊤ = ⊤

Tactic:
exacts [zero_mul _, one_mul _, top_mul_top]

Result:
no goals

Proof state:
y : ℝ
⊢ ((if 0 < y then 0 else if y = 0 then 1 else ⊤) * if 0 < y then 0 else if y = 0 then 1 else ⊤) =
    if 0 < y then 0 else if y = 0 then 1 else ⊤

Tactic:
split_ifs

Result:
case pos
y : ℝ
h✝ : 0 < y
⊢ 0 * 0 = 0

case pos
y : ℝ
h✝¹ : ¬0 < y
h✝ : y = 0
⊢ 1 * 1 = 1

case neg
y : ℝ
h✝¹ : ¬0 < y
h✝ : ¬y = 0
⊢ ⊤ * ⊤ = ⊤

Proof state:
y : ℝ
⊢ 0 ^ y * 0 ^ y = 0 ^ y

Tactic:
rw [zero_rpow_def]

Result:
y : ℝ
⊢ ((if 0 < y then 0 else if y = 0 then 1 else ⊤) * if 0 < y then 0 else if y = 0 then 1 else ⊤) =
    if 0 < y then 0 else if y = 0 then 1 else ⊤
-- Mathlib/Tactic/LinearCombination/Lemmas.lean
theorem le_of_eq [OrderedCancelAddCommMonoid α] (p : (a:α) = b) (H : a' + b ≤ b' + a) :
    a' ≤ b'

Proof state:
α : Type u_1
a a' b b' : α
inst✝ : OrderedCancelAddCommMonoid α
p : a = b
H : a' + b ≤ b' + a
⊢ a' ≤ b'

Tactic:
rwa [p, add_le_add_iff_right] at H

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem pderivCLM_eq_lineDeriv (m : E) (f : 𝓢(E, F)) (x : E) :
    pderivCLM 𝕜 m f x = lineDeriv ℝ f x m

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : E
f : 𝓢(E, F)
x : E
⊢ ((pderivCLM 𝕜 m) f) x = lineDeriv ℝ (⇑f) x m

Tactic:
simp only [pderivCLM_apply, f.differentiableAt.lineDeriv_eq_fderiv]

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr_redundant_pair (f : α → (σ × σ) → (σ × σ) × β)
    (h : ∀ x s, (f x (s, s)).fst.fst = (f x (s, s)).fst.snd) :
    (mapAccumr f xs (s, s)).snd = (mapAccumr (fun x (s : σ) =>
      (f x (s, s) |>.fst.fst, f x (s, s) |>.snd)
    ) xs s).snd :=
  mapAccumr_bisim_tail <| by
    use fun (s₁, s₂) s => s₂ = s ∧ s₁ = s
    simp_all

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
f : α → σ × σ → (σ × σ) × β
h : ∀ (x : α) (s : σ), (f x (s, s)).1.1 = (f x (s, s)).1.2
⊢ ∃ R,
    R (s, s) s ∧
      ∀ {s : σ × σ} {q : σ} (a : α),
        R s q → R (f a s).1 ((f a (q, q)).1.1, (f a (q, q)).2).1 ∧ (f a s).2 = ((f a (q, q)).1.1, (f a (q, q)).2).2

Tactic:
use fun (s₁, s₂) s => s₂ = s ∧ s₁ = s

Result:
case h
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
f : α → σ × σ → (σ × σ) × β
h : ∀ (x : α) (s : σ), (f x (s, s)).1.1 = (f x (s, s)).1.2
⊢ (fun x s =>
        match x with
        | (s₁, s₂) => s₂ = s ∧ s₁ = s)
      (s, s) s ∧
    ∀ {s : σ × σ} {q : σ} (a : α),
      (fun x s =>
            match x with
            | (s₁, s₂) => s₂ = s ∧ s₁ = s)
          s q →
        (fun x s =>
              match x with
              | (s₁, s₂) => s₂ = s ∧ s₁ = s)
            (f a s).1 ((f a (q, q)).1.1, (f a (q, q)).2).1 ∧
          (f a s).2 = ((f a (q, q)).1.1, (f a (q, q)).2).2

Proof state:
case h
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
f : α → σ × σ → (σ × σ) × β
h : ∀ (x : α) (s : σ), (f x (s, s)).1.1 = (f x (s, s)).1.2
⊢ (fun x s =>
        match x with
        | (s₁, s₂) => s₂ = s ∧ s₁ = s)
      (s, s) s ∧
    ∀ {s : σ × σ} {q : σ} (a : α),
      (fun x s =>
            match x with
            | (s₁, s₂) => s₂ = s ∧ s₁ = s)
          s q →
        (fun x s =>
              match x with
              | (s₁, s₂) => s₂ = s ∧ s₁ = s)
            (f a s).1 ((f a (q, q)).1.1, (f a (q, q)).2).1 ∧
          (f a s).2 = ((f a (q, q)).1.1, (f a (q, q)).2).2

Tactic:
simp_all

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
theorem Numeric.mul_pos (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hp₁ : 0 < x₁) (hp₂ : 0 < x₂) :
    0 < x₁ * x₂

Proof state:
x₁ x₂ : PGame
hx₁ : x₁.Numeric
hx₂ : x₂.Numeric
hp₁ : 0 < x₁
hp₂ : 0 < x₂
⊢ 0 < x₁ * x₂

Tactic:
rw [lt_iff_game_lt]

Result:
x₁ x₂ : PGame
hx₁ : x₁.Numeric
hx₂ : x₂.Numeric
hp₁ : 0 < x₁
hp₂ : 0 < x₂
⊢ ⟦0⟧ < ⟦x₁ * x₂⟧

Proof state:
x₁ x₂ : PGame
hx₁ : x₁.Numeric
hx₂ : x₂.Numeric
hp₁ : 0 < x₁
hp₂ : 0 < x₂
⊢ ⟦0⟧ < ⟦x₁ * x₂⟧

Tactic:
have := P3_of_lt_of_lt numeric_zero hx₁ numeric_zero hx₂ hp₁ hp₂

Result:
x₁ x₂ : PGame
hx₁ : x₁.Numeric
hx₂ : x₂.Numeric
hp₁ : 0 < x₁
hp₂ : 0 < x₂
this : P3 0 x₁ 0 x₂
⊢ ⟦0⟧ < ⟦x₁ * x₂⟧

Proof state:
x₁ x₂ : PGame
hx₁ : x₁.Numeric
hx₂ : x₂.Numeric
hp₁ : 0 < x₁
hp₂ : 0 < x₂
this : 0 < ⟦x₁ * x₂⟧
⊢ ⟦0⟧ < ⟦x₁ * x₂⟧

Tactic:
exact this

Result:
no goals

Proof state:
x₁ x₂ : PGame
hx₁ : x₁.Numeric
hx₂ : x₂.Numeric
hp₁ : 0 < x₁
hp₂ : 0 < x₂
this : P3 0 x₁ 0 x₂
⊢ ⟦0⟧ < ⟦x₁ * x₂⟧

Tactic:
simp_rw [P3, quot_zero_mul, quot_mul_zero, add_lt_add_iff_left] at this

Result:
x₁ x₂ : PGame
hx₁ : x₁.Numeric
hx₂ : x₂.Numeric
hp₁ : 0 < x₁
hp₂ : 0 < x₂
this : 0 < ⟦x₁ * x₂⟧
⊢ ⟦0⟧ < ⟦x₁ * x₂⟧
-- Mathlib/Data/Finset/SDiff.lean
theorem union_sdiff_symm : s ∪ t \ s = t ∪ s \ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s ∪ t \ s = t ∪ s \ t

Tactic:
simp [union_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSubVSubWeights_apply_of_ne [DecidableEq ι] {i j t : ι} (hi : t ≠ i) (hj : t ≠ j) :
    weightedVSubVSubWeights k i j t = 0

Proof state:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
inst✝ : DecidableEq ι
i j t : ι
hi : t ≠ i
hj : t ≠ j
⊢ weightedVSubVSubWeights k i j t = 0

Tactic:
simp [weightedVSubVSubWeights, hi, hj]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
lemma zero_zpow : ∀ n : ℤ, n ≠ 0 → (0 : G₀) ^ n = 0
  | (n : ℕ), h => by rw [zpow_natCast, zero_pow]; simpa [Int.natCast_eq_zero] using h
  | .negSucc n, _ => by simp

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ n ≠ 0

Tactic:
simpa [Int.natCast_eq_zero] using h

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ 0 ^ ↑n = 0

Tactic:
rw [zpow_natCast, zero_pow]

Result:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ n ≠ 0

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
x✝ : Int.negSucc n ≠ 0
⊢ 0 ^ Int.negSucc n = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem all_eq_true {p : α → Bool} {as : Array α} :
    as.all p = true ↔ ∀ (i : Nat) (_ : i < as.size), p as[i]

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ as.all p = true ↔ ∀ (i : Nat) (x : i < as.size), p as[i] = true

Tactic:
simp [all_iff_forall]

Result:
no goals
-- Mathlib/Data/Matroid/Dual.lean
theorem dual_coindep_iff : M✶.Coindep X ↔ M.Indep X

Proof state:
α : Type u_1
M : Matroid α
X : Set α
⊢ M✶.Coindep X ↔ M.Indep X

Tactic:
rw [Coindep, dual_dual]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem decide_forall_mem {l : List α} {p : α → Prop} [DecidablePred p] :
    decide (∀ x, x ∈ l → p x) = l.all p

Proof state:
α : Type u_1
l : List α
p : α → Prop
inst✝ : DecidablePred p
⊢ decide (∀ (x : α), x ∈ l → p x) = l.all fun b => decide (p b)

Tactic:
simp [all_eq]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
protected lemma EdgeDisjointTriangles.farFromTriangleFree (hG : G.EdgeDisjointTriangles)
    (tris_big : ε * (card α ^ 2 : ℕ) ≤ #(G.cliqueFinset 3)) :
    G.FarFromTriangleFree ε :=
  farFromTriangleFree_of_disjoint_triangles _ Subset.rfl (by simpa using hG) tris_big

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq α
hG : G.EdgeDisjointTriangles
tris_big : ε * ↑(Fintype.card α ^ 2) ≤ ↑(#(G.cliqueFinset 3))
⊢ (↑(G.cliqueFinset 3)).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton

Tactic:
simpa using hG

Result:
no goals
-- Mathlib/Data/Fin/Rev.lean
theorem rev_lt_iff {i j : Fin n} : rev i < j ↔ rev j < i

Proof state:
n : ℕ
i j : Fin n
⊢ i.rev < j ↔ j.rev < i

Tactic:
rw [← rev_lt_rev, rev_rev]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem coeFn_le (f g : Lp.simpleFunc G p μ) : (f : α → G) ≤ᵐ[μ] g ↔ f ≤ g

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝ : NormedLatticeAddCommGroup G
f g : ↥(simpleFunc G p μ)
⊢ ↑↑↑f ≤ᶠ[ae μ] ↑↑↑g ↔ f ≤ g

Tactic:
rw [← Subtype.coe_le_coe, ← Lp.coeFn_le]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Split.lean
theorem cofan_inj_comp_app (f : X ⟶ Y) {Δ : SimplexCategoryᵒᵖ} (A : IndexSet Δ) :
    (s.cofan Δ).inj A ≫ f.app Δ = s.φ f A.1.unop.len ≫ Y.map A.e.op

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : SimplicialObject C
s : Splitting X
f : X ⟶ Y
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ s.ι (unop A.fst).len ≫ X.map A.e.op ≫ f.app Δ = s.ι (unop A.fst).len ≫ f.app (op ⦋(unop A.fst).len⦌) ≫ Y.map A.e.op

Tactic:
rw [NatTrans.naturality]

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : SimplicialObject C
s : Splitting X
f : X ⟶ Y
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ f.app Δ = s.φ f (unop A.fst).len ≫ Y.map A.e.op

Tactic:
simp only [cofan_inj_eq_assoc, φ, assoc]

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : SimplicialObject C
s : Splitting X
f : X ⟶ Y
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ s.ι (unop A.fst).len ≫ X.map A.e.op ≫ f.app Δ = s.ι (unop A.fst).len ≫ f.app (op ⦋(unop A.fst).len⦌) ≫ Y.map A.e.op
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem mapTR_loop_eq (f : α → β) (as : List α) (bs : List β) :
    mapTR.loop f as bs = bs.reverse ++ map f as

Proof state:
case cons
α : Type u
β : Type v
f : α → β
a : α
as : List α
ih : ∀ (bs : List β), mapTR.loop f as bs = bs.reverse ++ map f as
bs : List β
⊢ bs.reverse ++ (f a :: nil ++ map f as) = bs.reverse ++ f a :: map f as

Tactic:
rfl

Result:
no goals

Proof state:
case nil
α : Type u
β : Type v
f : α → β
bs : List β
⊢ mapTR.loop f nil bs = bs.reverse ++ map f nil

Tactic:
simp [mapTR.loop, map]

Result:
no goals

Proof state:
case cons
α : Type u
β : Type v
f : α → β
a : α
as : List α
ih : ∀ (bs : List β), mapTR.loop f as bs = bs.reverse ++ map f as
bs : List β
⊢ mapTR.loop f as (f a :: bs) = bs.reverse ++ f a :: map f as

Tactic:
rw [ih (f a :: bs), reverse_cons, append_assoc]

Result:
case cons
α : Type u
β : Type v
f : α → β
a : α
as : List α
ih : ∀ (bs : List β), mapTR.loop f as bs = bs.reverse ++ map f as
bs : List β
⊢ bs.reverse ++ (f a :: nil ++ map f as) = bs.reverse ++ f a :: map f as

Proof state:
α : Type u
β : Type v
f : α → β
as : List α
bs : List β
⊢ mapTR.loop f as bs = bs.reverse ++ map f as

Tactic:
induction as generalizing bs with
| nil => simp [mapTR.loop, map]
| cons a as ih =>
  simp only [mapTR.loop, map]
  rw [ih (f a :: bs), reverse_cons, append_assoc]
  rfl

Result:
no goals

Proof state:
case cons
α : Type u
β : Type v
f : α → β
a : α
as : List α
ih : ∀ (bs : List β), mapTR.loop f as bs = bs.reverse ++ map f as
bs : List β
⊢ mapTR.loop f (a :: as) bs = bs.reverse ++ map f (a :: as)

Tactic:
simp only [mapTR.loop, map]

Result:
case cons
α : Type u
β : Type v
f : α → β
a : α
as : List α
ih : ∀ (bs : List β), mapTR.loop f as bs = bs.reverse ++ map f as
bs : List β
⊢ mapTR.loop f as (f a :: bs) = bs.reverse ++ f a :: map f as
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
protected lemma le_of_add_le_add_right [LE α] [AddRightReflectLE α] (hz : z ≠ ⊤) :
    x + z ≤ y + z → x ≤ y

Proof state:
α : Type u
inst✝² : Add α
x y z : WithTop α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
hz : z ≠ ⊤
⊢ x + z ≤ y + z → x ≤ y

Tactic:
lift z to α using hz

Result:
case intro
α : Type u
inst✝² : Add α
x y : WithTop α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z : α
⊢ x + ↑z ≤ y + ↑z → x ≤ y

Proof state:
case intro.coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z a✝¹ a✝ : α
⊢ a✝¹ + z ≤ a✝ + z → a✝¹ ≤ a✝

Tactic:
simpa using le_of_add_le_add_right

Result:
no goals

Proof state:
case intro
α : Type u
inst✝² : Add α
x y : WithTop α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z : α
⊢ x + ↑z ≤ y + ↑z → x ≤ y

Tactic:
cases x <;> cases y <;> simp [← coe_add]

Result:
case intro.coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z a✝¹ a✝ : α
⊢ a✝¹ + z ≤ a✝ + z → a✝¹ ≤ a✝
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem MeasureTheory.setIntegral_tsupport [TopologicalSpace X] :
    ∫ x in tsupport F, F x ∂ν = ∫ x, F x ∂ν

Proof state:
X : Type u_1
M : Type u_5
inst✝² : NormedAddCommGroup M
inst✝¹ : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
inst✝ : TopologicalSpace X
⊢ ∫ (x : X) in tsupport F, F x ∂ν = ∫ (x : X), F x ∂ν

Tactic:
nth_rw 2 [← setIntegral_univ]

Result:
X : Type u_1
M : Type u_5
inst✝² : NormedAddCommGroup M
inst✝¹ : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
inst✝ : TopologicalSpace X
⊢ ∫ (x : X) in tsupport F, F x ∂ν = ∫ (x : X) in univ, F x ∂ν

Proof state:
X : Type u_1
M : Type u_5
inst✝² : NormedAddCommGroup M
inst✝¹ : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
inst✝ : TopologicalSpace X
⊢ ∀ x ∈ univ \ tsupport F, F x = 0

Tactic:
exact fun _ hx => image_eq_zero_of_nmem_tsupport <| not_mem_of_mem_diff hx

Result:
no goals

Proof state:
X : Type u_1
M : Type u_5
inst✝² : NormedAddCommGroup M
inst✝¹ : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
inst✝ : TopologicalSpace X
⊢ ∫ (x : X) in tsupport F, F x ∂ν = ∫ (x : X) in univ, F x ∂ν

Tactic:
rw [setIntegral_eq_of_subset_of_forall_diff_eq_zero MeasurableSet.univ (subset_univ (tsupport F))]

Result:
X : Type u_1
M : Type u_5
inst✝² : NormedAddCommGroup M
inst✝¹ : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
inst✝ : TopologicalSpace X
⊢ ∀ x ∈ univ \ tsupport F, F x = 0
-- Mathlib/Analysis/MeanInequalitiesPow.lean
theorem rpow_arith_mean_le_arith_mean2_rpow (w₁ w₂ z₁ z₂ : ℝ≥0) (hw' : w₁ + w₂ = 1) {p : ℝ}
    (hp : 1 ≤ p) : (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p

Proof state:
case refine_1
w₁ w₂ z₁ z₂ : ℝ≥0
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i = 1

Tactic:
simp [hw', Fin.sum_univ_succ]

Result:
no goals

Proof state:
w₁ w₂ z₁ z₂ : ℝ≥0
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p

Tactic:
have h := rpow_arith_mean_le_arith_mean_rpow univ ![w₁, w₂] ![z₁, z₂] ?_ hp

Result:
case refine_2
w₁ w₂ z₁ z₂ : ℝ≥0
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
h :
  (∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i) ^ p ≤
    ∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i ^ p
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p

case refine_1
w₁ w₂ z₁ z₂ : ℝ≥0
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i = 1

Proof state:
case refine_2
w₁ w₂ z₁ z₂ : ℝ≥0
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
h :
  (∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i) ^ p ≤
    ∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i ^ p
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p

Tactic:
simpa [Fin.sum_univ_succ] using h

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/PureCoherence.lean
theorem naturality_id {p f pf : C} (η_f : p ⊗ f ≅ pf) :
    p ◁ Iso.refl f ≪≫ η_f = η_f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f pf : C
η_f : p ⊗ f ≅ pf
⊢ p ◁ Iso.refl f ≪≫ η_f = η_f

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem inv_smul (k : α) [Invertible k] (h : IsUnit A.det) : (k • A)⁻¹ = ⅟ k • A⁻¹ :=
  inv_eq_left_inv (by simp [h, smul_smul])

Proof state:
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
k : α
inst✝ : Invertible k
h : IsUnit A.det
⊢ ⅟k • A⁻¹ * k • A = 1

Tactic:
simp [h, smul_smul]

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem mgf_sum_of_identDistrib
    {X : ι → Ω → ℝ}
    {s : Finset ι} {j : ι}
    (h_meas : ∀ i, Measurable (X i))
    (h_indep : iIndepFun (fun _ => inferInstance) X μ)
    (hident : ∀ i ∈ s, ∀ j ∈ s, IdentDistrib (X i) (X j) μ μ)
    (hj : j ∈ s) (t : ℝ) : mgf (∑ i ∈ s, X i) μ t = mgf (X j) μ t ^ #s

Proof state:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ι → Ω → ℝ
s : Finset ι
j : ι
h_meas : ∀ (i : ι), Measurable (X i)
h_indep : iIndepFun (fun x => inferInstance) X μ
hident : ∀ i ∈ s, ∀ j ∈ s, IdentDistrib (X i) (X j) μ μ
hj : j ∈ s
t : ℝ
⊢ mgf (∑ i ∈ s, X i) μ t = mgf (X j) μ t ^ #s

Tactic:
rw [h_indep.mgf_sum h_meas]

Result:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ι → Ω → ℝ
s : Finset ι
j : ι
h_meas : ∀ (i : ι), Measurable (X i)
h_indep : iIndepFun (fun x => inferInstance) X μ
hident : ∀ i ∈ s, ∀ j ∈ s, IdentDistrib (X i) (X j) μ μ
hj : j ∈ s
t : ℝ
⊢ ∏ i ∈ s, mgf (X i) μ t = mgf (X j) μ t ^ #s

Proof state:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ι → Ω → ℝ
s : Finset ι
j : ι
h_meas : ∀ (i : ι), Measurable (X i)
h_indep : iIndepFun (fun x => inferInstance) X μ
hident : ∀ i ∈ s, ∀ j ∈ s, IdentDistrib (X i) (X j) μ μ
hj : j ∈ s
t : ℝ
⊢ ∏ i ∈ s, mgf (X i) μ t = mgf (X j) μ t ^ #s

Tactic:
exact Finset.prod_eq_pow_card fun i hi =>
  mgf_congr_of_identDistrib (X i) (X j) (hident i hi j hj) t

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_subset_Ioo_left (h : a₁ < a₂) : Ico a₂ b ⊆ Ioo a₁ b

Proof state:
α : Type u_2
a₁ a₂ b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : a₁ < a₂
⊢ Ico a₂ b ⊆ Ioo a₁ b

Tactic:
rw [← coe_subset, coe_Ico, coe_Ioo]

Result:
α : Type u_2
a₁ a₂ b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : a₁ < a₂
⊢ Set.Ico a₂ b ⊆ Set.Ioo a₁ b

Proof state:
α : Type u_2
a₁ a₂ b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : a₁ < a₂
⊢ Set.Ico a₂ b ⊆ Set.Ioo a₁ b

Tactic:
exact Set.Ico_subset_Ioo_left h

Result:
no goals
-- Mathlib/Data/List/Forall2.lean
theorem forall₂_take_append (l : List α) (l₁ : List β) (l₂ : List β) (h : Forall₂ R l (l₁ ++ l₂)) :
    Forall₂ R (List.take (length l₁) l) l₁

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (take l₁.length l) (take l₁.length (l₁ ++ l₂))
⊢ Forall₂ R (take l₁.length l) l₁

Tactic:
rwa [take_left] at h'

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
⊢ Forall₂ R (take l₁.length l) l₁

Tactic:
have h' : Forall₂ R (take (length l₁) l) (take (length l₁) (l₁ ++ l₂)) :=
  forall₂_take (length l₁) h

Result:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (take l₁.length l) (take l₁.length (l₁ ++ l₂))
⊢ Forall₂ R (take l₁.length l) l₁
-- Mathlib/RingTheory/HahnSeries/Addition.lean
@[simp]
protected lemma map_neg [AddGroup S] (f : R →+ S) {x : HahnSeries Γ R} :
    ((-x).map f : HahnSeries Γ S) = -(x.map f)

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : AddGroup S
f : R →+ S
x : HahnSeries Γ R
x✝ : Γ
⊢ ((-x).map f).coeff x✝ = (-x.map f).coeff x✝

Tactic:
simp

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : AddGroup S
f : R →+ S
x : HahnSeries Γ R
⊢ (-x).map f = -x.map f

Tactic:
ext

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : AddGroup S
f : R →+ S
x : HahnSeries Γ R
x✝ : Γ
⊢ ((-x).map f).coeff x✝ = (-x.map f).coeff x✝
-- Mathlib/Data/Complex/Basic.lean
theorem mul_inv_cancel {z : ℂ} (h : z ≠ 0) : z * z⁻¹ = 1

Proof state:
z : ℂ
h : z ≠ 0
⊢ z * z⁻¹ = 1

Tactic:
rw [inv_def, ← mul_assoc, mul_conj, ← ofReal_mul, mul_inv_cancel₀ (mt normSq_eq_zero.1 h),
  ofReal_one]

Result:
no goals
-- Mathlib/RingTheory/Finiteness/Cardinality.lean
lemma _root_.Module.finite_of_finite [Finite R] [Module.Finite R M] : Finite M

Proof state:
case intro.intro
R : Type u
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Finite R
inst✝ : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Surjective ⇑f
⊢ Finite M

Tactic:
exact .of_surjective f hf

Result:
no goals

Proof state:
R : Type u
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Finite R
inst✝ : Module.Finite R M
⊢ Finite M

Tactic:
obtain ⟨n, f, hf⟩ := exists_fin' R M

Result:
case intro.intro
R : Type u
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Finite R
inst✝ : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Surjective ⇑f
⊢ Finite M
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem nfpBFamily_lt_ord {o : Ordinal} {f : ∀ a < o, Ordinal → Ordinal} {c} (hc : ℵ₀ < cof c)
    (hc' : o.card < cof c) (hf : ∀ (i hi), ∀ b < c, f i hi b < c) {a} :
    a < c → nfpBFamily.{u, u} o f a < c :=
  nfpBFamily_lt_ord_lift hc (by rwa [o.card.lift_id]) hf

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u} → Ordinal.{u}
c : Ordinal.{u}
hc : ℵ₀ < c.cof
hc' : o.card < c.cof
hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c, f i hi b < c
a : Ordinal.{u}
⊢ Cardinal.lift.{u, u} o.card < c.cof

Tactic:
rwa [o.card.lift_id]

Result:
no goals