harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SetFamily/KruskalKatona.lean
theorem iterated_kk (h₁ : (𝒜 : Set (Finset (Fin n))).Sized r) (h₂ : #𝒞 ≤ #𝒜) (h₃ : IsInitSeg 𝒞 r) :
    #(∂^[k] 𝒞) ≤ #(∂^[k] 𝒜)

Proof state:
case succ
n n✝ : ℕ
ih : ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))}, Set.Sized r ↑𝒜 → #𝒞 ≤ #𝒜 → IsInitSeg 𝒞 r → #(∂ ^[n✝] 𝒞) ≤ #(∂ ^[n✝] 𝒜)
r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
⊢ IsInitSeg (∂ 𝒞) (r - 1)

Tactic:
convert h₃.shadow

Result:
no goals

Proof state:
n r k : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
⊢ #(∂ ^[k] 𝒞) ≤ #(∂ ^[k] 𝒜)

Tactic:
induction k generalizing r 𝒜 𝒞 with
| zero => simpa
| succ _ ih =>
  refine ih h₁.shadow (kruskal_katona h₁ h₂ h₃) ?_
  convert h₃.shadow

Result:
no goals

Proof state:
case zero
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
⊢ #(∂ ^[0] 𝒞) ≤ #(∂ ^[0] 𝒜)

Tactic:
simpa

Result:
no goals

Proof state:
case succ
n n✝ : ℕ
ih : ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))}, Set.Sized r ↑𝒜 → #𝒞 ≤ #𝒜 → IsInitSeg 𝒞 r → #(∂ ^[n✝] 𝒞) ≤ #(∂ ^[n✝] 𝒜)
r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
⊢ #(∂ ^[n✝ + 1] 𝒞) ≤ #(∂ ^[n✝ + 1] 𝒜)

Tactic:
refine ih h₁.shadow (kruskal_katona h₁ h₂ h₃) ?_

Result:
case succ
n n✝ : ℕ
ih : ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))}, Set.Sized r ↑𝒜 → #𝒞 ≤ #𝒜 → IsInitSeg 𝒞 r → #(∂ ^[n✝] 𝒞) ≤ #(∂ ^[n✝] 𝒜)
r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
⊢ IsInitSeg (∂ 𝒞) (r - 1)
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem derivative_nodal [DecidableEq ι] :
    derivative (nodal s v) = ∑ i ∈ s, nodal (s.erase i) v

Proof state:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
t : Finset ι
hit : i ∉ t
IH : derivative (nodal t v) = ∑ i ∈ t, nodal (t.erase i) v
⊢ derivative (nodal (insert i t) v) = ∑ i_1 ∈ insert i t, nodal ((insert i t).erase i_1) v

Tactic:
rw [nodal_insert_eq_nodal hit, derivative_mul, IH, derivative_sub, derivative_X, derivative_C,
  sub_zero, one_mul, sum_insert hit, mul_sum, erase_insert hit, add_right_inj]

Result:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
t : Finset ι
hit : i ∉ t
IH : derivative (nodal t v) = ∑ i ∈ t, nodal (t.erase i) v
⊢ ∑ i_1 ∈ t, (X - C (v i)) * nodal (t.erase i_1) v = ∑ x ∈ t, nodal ((insert i t).erase x) v

Proof state:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
⊢ derivative (nodal ∅ v) = ∑ i ∈ ∅, nodal (∅.erase i) v

Tactic:
rw [nodal_empty, derivative_one, sum_empty]

Result:
no goals

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

Tactic:
refine s.induction_on ?_ fun i t hit IH => ?_

Result:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
⊢ derivative (nodal ∅ v) = ∑ i ∈ ∅, nodal (∅.erase i) v

case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
t : Finset ι
hit : i ∉ t
IH : derivative (nodal t v) = ∑ i ∈ t, nodal (t.erase i) v
⊢ derivative (nodal (insert i t) v) = ∑ i_1 ∈ insert i t, nodal ((insert i t).erase i_1) v

Proof state:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
t : Finset ι
hit : i ∉ t
IH : derivative (nodal t v) = ∑ i ∈ t, nodal (t.erase i) v
j : ι
hjt : j ∈ t
⊢ (X - C (v i)) * nodal (t.erase j) v = nodal ((insert i t).erase j) v

Tactic:
rw [t.erase_insert_of_ne (ne_of_mem_of_not_mem hjt hit).symm,
  nodal_insert_eq_nodal (mem_of_mem_erase.mt hit)]

Result:
no goals

Proof state:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
t : Finset ι
hit : i ∉ t
IH : derivative (nodal t v) = ∑ i ∈ t, nodal (t.erase i) v
⊢ ∑ i_1 ∈ t, (X - C (v i)) * nodal (t.erase i_1) v = ∑ x ∈ t, nodal ((insert i t).erase x) v

Tactic:
refine sum_congr rfl fun j hjt => ?_

Result:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
t : Finset ι
hit : i ∉ t
IH : derivative (nodal t v) = ∑ i ∈ t, nodal (t.erase i) v
j : ι
hjt : j ∈ t
⊢ (X - C (v i)) * nodal (t.erase j) v = nodal ((insert i t).erase j) v
-- Mathlib/Topology/Partial.lean
theorem open_dom_of_pcontinuous {f : X →. Y} (h : PContinuous f) : IsOpen f.Dom

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
h : PContinuous f
⊢ IsOpen (f.preimage Set.univ)

Tactic:
exact h _ isOpen_univ

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
h : PContinuous f
⊢ IsOpen f.Dom

Tactic:
rw [← PFun.preimage_univ]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
h : PContinuous f
⊢ IsOpen (f.preimage Set.univ)
-- Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean
lemma hasReflexiveCoequalizer_iff_hasCoequalizer :
    HasColimit F ↔ HasCoequalizer (F.map left) (F.map right)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
⊢ HasColimit F ↔ HasCoequalizer (F.map left) (F.map right)

Tactic:
simpa only [hasColimit_iff_hasInitial_cocone]
  using Equivalence.hasInitial_iff (reflexiveCoforkEquivCofork F)

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
@[simp]
lemma rightHomologyMap'_neg :
    rightHomologyMap' (-φ) h₁ h₂ = -rightHomologyMap' φ h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' (-φ) h₁ h₂ = -rightHomologyMap' φ h₁ h₂

Tactic:
have γ : RightHomologyMapData φ h₁ h₂ := default

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ rightHomologyMap' (-φ) h₁ h₂ = -rightHomologyMap' φ h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ rightHomologyMap' (-φ) h₁ h₂ = -rightHomologyMap' φ h₁ h₂

Tactic:
simp only [γ.rightHomologyMap'_eq, γ.neg.rightHomologyMap'_eq, RightHomologyMapData.neg_φH]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem c₄_of_isCharNeTwoNF : W.c₄ = 16 * W.a₂ ^ 2 - 48 * W.a₄

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ (4 * W.a₂) ^ 2 - 24 * (2 * W.a₄) = 16 * W.a₂ ^ 2 - 48 * W.a₄

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.c₄ = 16 * W.a₂ ^ 2 - 48 * W.a₄

Tactic:
rw [c₄, b₂_of_isCharNeTwoNF, b₄_of_isCharNeTwoNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ (4 * W.a₂) ^ 2 - 24 * (2 * W.a₄) = 16 * W.a₂ ^ 2 - 48 * W.a₄
-- Mathlib/Data/List/Sym.lean
theorem left_mem_of_mk_mem_sym2 {xs : List α} {a b : α}
    (h : s(a, b) ∈ xs.sym2) : a ∈ xs

Proof state:
case cons.inl
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : s(a, b) = s(x, x)
⊢ a = x ∨ a ∈ xs

Tactic:
rw [Sym2.eq_iff, ← and_or_left] at h

Result:
case cons.inl
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : a = x ∧ (b = x ∨ b = x)
⊢ a = x ∨ a ∈ xs

Proof state:
case cons.inl
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : a = x ∧ (b = x ∨ b = x)
⊢ a = x ∨ a ∈ xs

Tactic:
exact .inl h.1

Result:
no goals

Proof state:
case cons.inr.inl.intro.intro
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
c : α
hc : c ∈ xs
h : a = x ∧ b = c ∨ a = c ∧ b = x
⊢ a = x ∨ a ∈ xs

Tactic:
obtain (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) := h <;> simp [hc]

Result:
no goals

Proof state:
case cons.inr.inr
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : s(a, b) ∈ xs.sym2
⊢ a = x ∨ a ∈ xs

Tactic:
exact .inr <| ih h

Result:
no goals

Proof state:
case cons
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : s(a, b) ∈ (x :: xs).sym2
⊢ a = x ∨ a ∈ xs

Tactic:
rw [mem_sym2_cons_iff] at h

Result:
case cons
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : s(a, b) = s(x, x) ∨ (∃ y ∈ xs, s(a, b) = s(x, y)) ∨ s(a, b) ∈ xs.sym2
⊢ a = x ∨ a ∈ xs

Proof state:
case cons
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : s(a, b) ∈ (x :: xs).sym2
⊢ a ∈ x :: xs

Tactic:
rw [mem_cons]

Result:
case cons
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : s(a, b) ∈ (x :: xs).sym2
⊢ a = x ∨ a ∈ xs

Proof state:
case nil
α : Type u_1
a b : α
h : s(a, b) ∈ [].sym2
⊢ a ∈ []

Tactic:
exact (not_mem_nil _ h).elim

Result:
no goals

Proof state:
case cons.inr.inl.intro.intro
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
c : α
hc : c ∈ xs
h : s(a, b) = s(x, c)
⊢ a = x ∨ a ∈ xs

Tactic:
rw [Sym2.eq_iff] at h

Result:
case cons.inr.inl.intro.intro
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
c : α
hc : c ∈ xs
h : a = x ∧ b = c ∨ a = c ∧ b = x
⊢ a = x ∨ a ∈ xs

Proof state:
case cons
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : s(a, b) = s(x, x) ∨ (∃ y ∈ xs, s(a, b) = s(x, y)) ∨ s(a, b) ∈ xs.sym2
⊢ a = x ∨ a ∈ xs

Tactic:
obtain (h | ⟨c, hc, h⟩ | h) := h

Result:
case cons.inl
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : s(a, b) = s(x, x)
⊢ a = x ∨ a ∈ xs

case cons.inr.inl.intro.intro
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
c : α
hc : c ∈ xs
h : s(a, b) = s(x, c)
⊢ a = x ∨ a ∈ xs

case cons.inr.inr
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : s(a, b) ∈ xs.sym2
⊢ a = x ∨ a ∈ xs
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_signExtend (x : BitVec w) {v : Nat} :
    (x.signExtend v).toNat = (x.setWidth v).toNat + if x.msb then 2^v - 2^w else 0

Proof state:
case neg
w : Nat
x : BitVec w
v : Nat
h : ¬v ≤ w
⊢ (signExtend v x).toNat = (setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0

Tactic:
have : 2^w ≤ 2^v := Nat.pow_le_pow_of_le_right Nat.two_pos (by omega)

Result:
case neg
w : Nat
x : BitVec w
v : Nat
h : ¬v ≤ w
this : 2 ^ w ≤ 2 ^ v
⊢ (signExtend v x).toNat = (setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0

Proof state:
case pos
w : Nat
x : BitVec w
v : Nat
h : v ≤ w
⊢ (signExtend v x).toNat = (setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0

Tactic:
have : 2^v ≤ 2^w := Nat.pow_le_pow_of_le_right Nat.two_pos h

Result:
case pos
w : Nat
x : BitVec w
v : Nat
h : v ≤ w
this : 2 ^ v ≤ 2 ^ w
⊢ (signExtend v x).toNat = (setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0

Proof state:
w : Nat
x : BitVec w
v : Nat
h : ¬v ≤ w
this : 2 ^ w ≤ 2 ^ v
⊢ w ≤ v

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
v : Nat
⊢ (signExtend v x).toNat = (setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0

Tactic:
by_cases h : v ≤ w

Result:
case pos
w : Nat
x : BitVec w
v : Nat
h : v ≤ w
⊢ (signExtend v x).toNat = (setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0

case neg
w : Nat
x : BitVec w
v : Nat
h : ¬v ≤ w
⊢ (signExtend v x).toNat = (setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0

Proof state:
w : Nat
x : BitVec w
v : Nat
h : ¬v ≤ w
this : 2 ^ w ≤ 2 ^ v
⊢ x.toNat < 2 ^ v

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
v : Nat
h : ¬v ≤ w
⊢ w ≤ v

Tactic:
omega

Result:
no goals

Proof state:
case pos
w : Nat
x : BitVec w
v : Nat
h : v ≤ w
this : 2 ^ v ≤ 2 ^ w
⊢ (signExtend v x).toNat = (setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0

Tactic:
simp [signExtend_eq_setWidth_of_lt x h, toNat_setWidth, Nat.sub_eq_zero_of_le this]

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
v : Nat
h : ¬v ≤ w
this : 2 ^ w ≤ 2 ^ v
⊢ (signExtend v x).toNat = (setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0

Tactic:
rw [toNat_signExtend_of_le x (by omega), toNat_setWidth, Nat.mod_eq_of_lt (by omega)]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
theorem lpMeasSubgroupToLpTrim_norm_map [hp : Fact (1 ≤ p)] (hm : m ≤ m0)
    (f : lpMeasSubgroup F m p μ) : ‖lpMeasSubgroupToLpTrim F p μ hm f‖ = ‖f‖

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hp : Fact (1 ≤ p)
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ ‖↑f‖ = ‖f‖

Tactic:
congr

Result:
no goals

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hp : Fact (1 ≤ p)
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ ‖lpMeasSubgroupToLpTrim F p μ hm f‖ = ‖f‖

Tactic:
rw [Lp.norm_def, eLpNorm_trim hm (Lp.stronglyMeasurable _),
  eLpNorm_congr_ae (lpMeasSubgroupToLpTrim_ae_eq hm _), ← Lp.norm_def]

Result:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hp : Fact (1 ≤ p)
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ ‖↑f‖ = ‖f‖
-- Mathlib/CategoryTheory/GradedObject/Monoidal.lean
@[reassoc]
lemma ιTensorObj₃'_eq (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) (i₁₂ : I)
    (h' : i₁ + i₂ = i₁₂) :
    ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h =
      (ιTensorObj X₁ X₂ i₁ i₂ i₁₂ h' ▷ X₃ i₃) ≫
        ιTensorObj (tensorObj X₁ X₂) X₃ i₁₂ i₃ j (by rw [← h', h])

Proof state:
I : Type u
inst✝⁴ : AddMonoid I
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : MonoidalCategory C
X₁ X₂ X₃ : GradedObject I C
inst✝¹ : X₁.HasTensor X₂
inst✝ : (tensorObj X₁ X₂).HasTensor X₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h =
    ιTensorObj X₁ X₂ i₁ i₂ (i₁ + i₂) ⋯ ▷ X₃ i₃ ≫ ιTensorObj (tensorObj X₁ X₂) X₃ (i₁ + i₂) i₃ j ⋯

Tactic:
rfl

Result:
no goals

Proof state:
I : Type u
inst✝⁴ : AddMonoid I
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : MonoidalCategory C
X₁ X₂ X₃ : GradedObject I C
inst✝¹ : X₁.HasTensor X₂
inst✝ : (tensorObj X₁ X₂).HasTensor X₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₁₂ : I
h' : i₁ + i₂ = i₁₂
⊢ ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h =
    ιTensorObj X₁ X₂ i₁ i₂ i₁₂ h' ▷ X₃ i₃ ≫ ιTensorObj (tensorObj X₁ X₂) X₃ i₁₂ i₃ j ⋯

Tactic:
subst h'

Result:
I : Type u
inst✝⁴ : AddMonoid I
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : MonoidalCategory C
X₁ X₂ X₃ : GradedObject I C
inst✝¹ : X₁.HasTensor X₂
inst✝ : (tensorObj X₁ X₂).HasTensor X₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h =
    ιTensorObj X₁ X₂ i₁ i₂ (i₁ + i₂) ⋯ ▷ X₃ i₃ ≫ ιTensorObj (tensorObj X₁ X₂) X₃ (i₁ + i₂) i₃ j ⋯

Proof state:
I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{?u.104950, u_1} C
inst✝⁴ : MonoidalCategory C
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₁.HasTensor X₂
inst✝² : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹ : Y₁.HasTensor Y₂
inst✝ : (tensorObj Y₁ Y₂).HasTensor Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₁₂ : I
h' : i₁ + i₂ = i₁₂
⊢ i₁₂ + i₃ = j

Tactic:
rw [← h', h]

Result:
no goals
-- Mathlib/Probability/Moments/MGFAnalytic.lean
lemma analyticAt_cgf (h : v ∈ interior (integrableExpSet X μ)) : AnalyticAt ℝ (cgf X μ) v

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ AnalyticAt ℝ 0 v

Tactic:
exact analyticAt_const

Result:
no goals

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ AnalyticAt ℝ (cgf X μ) v

Tactic:
exact (analyticAt_mgf h).log <| mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)

Result:
no goals

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ AnalyticAt ℝ (cgf X μ) v

Tactic:
simp only [hμ, cgf_zero_measure]

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ AnalyticAt ℝ 0 v

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
⊢ AnalyticAt ℝ (cgf X μ) v

Tactic:
by_cases hμ : μ = 0

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ AnalyticAt ℝ (cgf X μ) v

case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ AnalyticAt ℝ (cgf X μ) v
-- Mathlib/Logic/IsEmpty.lean
theorem isEmpty_plift {α} : IsEmpty (PLift α) ↔ IsEmpty α

Proof state:
α : Sort u_4
⊢ IsEmpty (PLift α) ↔ IsEmpty α

Tactic:
simp only [← not_nonempty_iff, nonempty_plift]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_eq_iff_sdiff_eq (ha : a ≤ c) : a ∆ b = c ↔ c \ a = b

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
ha : a ≤ c
⊢ a ∆ b = c ↔ a ∆ c = b

Tactic:
exact ((symmDiff_right_involutive a).toPerm _).apply_eq_iff_eq_symm_apply.trans eq_comm

Result:
no goals

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
ha : a ≤ c
⊢ a ∆ b = c ↔ c \ a = b

Tactic:
rw [← symmDiff_of_le ha]

Result:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
ha : a ≤ c
⊢ a ∆ b = c ↔ a ∆ c = b
-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem affineSpan_pair_eq_altitude_iff {n : ℕ} (s : Simplex ℝ P (n + 1)) (i : Fin (n + 2))
    (p : P) :
    line[ℝ, p, s.points i] = s.altitude i ↔
      p ≠ s.points i ∧
        p ∈ affineSpan ℝ (Set.range s.points) ∧
          p -ᵥ s.points i ∈ (affineSpan ℝ (s.points '' ↑(Finset.univ.erase i))).directionᗮ

Proof state:
case mpr.intro.refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ LinearIndepOn ℝ id {p -ᵥ s.points i}

Tactic:
exact LinearIndepOn.id_singleton _ <| by simpa using hne

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma zero_eq_ofENat {m : ℕ∞} : 0 = (m : Cardinal) ↔ m = 0

Proof state:
m : ℕ∞
⊢ 0 = m ↔ m = 0

Tactic:
apply eq_comm

Result:
no goals

Proof state:
m : ℕ∞
⊢ 0 = ↑m ↔ m = 0

Tactic:
norm_cast

Result:
m : ℕ∞
⊢ 0 = m ↔ m = 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_unitOfList [EquivBEq α] [LawfulHashable α]
    {l : List α} {k : α} :
    k ∈ unitOfList l ↔ l.contains k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k : α
⊢ k ∈ unitOfList l ↔ l.contains k = true

Tactic:
simp [mem_iff_contains]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem eq_of_getLsbD_eq {x y : BitVec w}
    (pred : ∀ i, i < w → x.getLsbD i = y.getLsbD i) : x = y

Proof state:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i
⊢ x = y

Tactic:
apply eq_of_toNat_eq

Result:
case a
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i
⊢ x.toNat = y.toNat

Proof state:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i
i : Nat
i_lt : i < w
⊢ x.toNat.testBit i = y.toNat.testBit i

Tactic:
exact pred i i_lt

Result:
no goals

Proof state:
case a.pred
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i
⊢ ∀ (i : Nat), x.toNat.testBit i = y.toNat.testBit i

Tactic:
intro i

Result:
case a.pred
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i
i : Nat
⊢ x.toNat.testBit i = y.toNat.testBit i

Proof state:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i
i : Nat
i_lt : ¬i < w
p : i ≥ w
⊢ x.toNat.testBit i = y.toNat.testBit i

Tactic:
simp [testBit_toNat, getLsbD_ge _ _ p]

Result:
no goals

Proof state:
case a.pred
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i
i : Nat
⊢ x.toNat.testBit i = y.toNat.testBit i

Tactic:
if i_lt : i < w then
  exact pred i i_lt
else
  have p : i ≥ w := Nat.le_of_not_gt i_lt
  simp [testBit_toNat, getLsbD_ge _ _ p]

Result:
no goals

Proof state:
case a
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i
⊢ x.toNat = y.toNat

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case a.pred
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i
⊢ ∀ (i : Nat), x.toNat.testBit i = y.toNat.testBit i

Proof state:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i
i : Nat
i_lt : ¬i < w
⊢ x.toNat.testBit i = y.toNat.testBit i

Tactic:
have p : i ≥ w := Nat.le_of_not_gt i_lt

Result:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i
i : Nat
i_lt : ¬i < w
p : i ≥ w
⊢ x.toNat.testBit i = y.toNat.testBit i
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_filter (p : α → Prop) [DecidablePred p] (f : α → β) :
    ∏ a ∈ s with p a, f a = ∏ a ∈ s, if p a then f a else 1 :=
  calc
    ∏ a ∈ s with p a, f a = ∏ a ∈ s with p a, if p a then f a else 1 :=
      prod_congr rfl fun a h => by rw [if_pos]; simpa using (mem_filter.1 h).2
    _ = ∏ a ∈ s, if p a then f a else 1

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
inst✝¹ : CommMonoid β
p : α → Prop
inst✝ : DecidablePred p
f : α → β
a : α
h : a ∈ filter (fun a => p a) s
⊢ f a = if p a then f a else 1

Tactic:
rw [if_pos]

Result:
case hc
α : Type u_3
β : Type u_4
s : Finset α
inst✝¹ : CommMonoid β
p : α → Prop
inst✝ : DecidablePred p
f : α → β
a : α
h : a ∈ filter (fun a => p a) s
⊢ p a

Proof state:
case hc
α : Type u_3
β : Type u_4
s : Finset α
inst✝¹ : CommMonoid β
p : α → Prop
inst✝ : DecidablePred p
f : α → β
a : α
h : a ∈ filter (fun a => p a) s
⊢ p a

Tactic:
simpa using (mem_filter.1 h).2

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
inst✝¹ : CommMonoid β
p : α → Prop
inst✝ : DecidablePred p
f : α → β
x : α
hs : x ∈ s
h : x ∈ s → ¬p x
⊢ (if p x then f x else 1) = 1

Tactic:
exact if_neg (by simpa using h hs)

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
inst✝¹ : CommMonoid β
p : α → Prop
inst✝ : DecidablePred p
f : α → β
⊢ (∏ a ∈ filter (fun a => p a) s, if p a then f a else 1) = ∏ a ∈ s, if p a then f a else 1

Tactic:
refine prod_subset (filter_subset _ s) fun x hs h => ?_

Result:
α : Type u_3
β : Type u_4
s : Finset α
inst✝¹ : CommMonoid β
p : α → Prop
inst✝ : DecidablePred p
f : α → β
x : α
hs : x ∈ s
h : x ∉ filter (fun a => p a) s
⊢ (if p x then f x else 1) = 1

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
inst✝¹ : CommMonoid β
p : α → Prop
inst✝ : DecidablePred p
f : α → β
x : α
hs : x ∈ s
h : x ∈ s → ¬p x
⊢ ¬p x

Tactic:
simpa using h hs

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
inst✝¹ : CommMonoid β
p : α → Prop
inst✝ : DecidablePred p
f : α → β
x : α
hs : x ∈ s
h : x ∉ filter (fun a => p a) s
⊢ (if p x then f x else 1) = 1

Tactic:
rw [mem_filter, not_and] at h

Result:
α : Type u_3
β : Type u_4
s : Finset α
inst✝¹ : CommMonoid β
p : α → Prop
inst✝ : DecidablePred p
f : α → β
x : α
hs : x ∈ s
h : x ∈ s → ¬p x
⊢ (if p x then f x else 1) = 1