harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lift_is_succ {o : Ordinal.{v}} : (∃ a, lift.{u} o = succ a) ↔ ∃ a, o = succ a :=
  ⟨fun ⟨a, h⟩ =>
    let ⟨b, e⟩ := mem_range_lift_of_le <| show a ≤ lift.{u} o from le_of_lt <| h.symm ▸ lt_succ a
    ⟨b, (lift_inj.{u,v}).1 <| by rw [h, ← e, lift_succ]⟩,
    fun ⟨a, h⟩ => ⟨lift.{u} a, by simp only [h, lift_succ]⟩⟩

Proof state:
o : Ordinal.{v}
x✝ : ∃ a, o = succ a
a : Ordinal.{v}
h : o = succ a
⊢ lift.{u, v} o = succ (lift.{u, v} a)

Tactic:
simp only [h, lift_succ]

Result:
no goals

Proof state:
o : Ordinal.{v}
x✝ : ∃ a, lift.{u, v} o = succ a
a : Ordinal.{max v u}
h : lift.{u, v} o = succ a
b : Ordinal.{v}
e : lift.{u, v} b = a
⊢ lift.{u, v} o = lift.{u, v} (succ b)

Tactic:
rw [h, ← e, lift_succ]

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem limitRecOn_of_isSuccLimit (hb : IsSuccLimit b) :
    limitRecOn b hm hs hl = hl b hb fun x _ ↦ limitRecOn x hm hs hl

Proof state:
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hm : (a : α) → IsMin a → C a
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccLimit a → ((b : α) → b < a → C b) → C a
hb : IsSuccLimit b
⊢ limitRecOn b hm hs hl = hl b hb fun x x_1 => limitRecOn x hm hs hl

Tactic:
rw [limitRecOn, prelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_neg hb.not_isMin]

Result:
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hm : (a : α) → IsMin a → C a
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccLimit a → ((b : α) → b < a → C b) → C a
hb : IsSuccLimit b
⊢ (hl b ⋯ fun x x_1 => prelimitRecOn x hs fun a ha IH => if h : IsMin a then hm a h else hl a ⋯ IH) =
    hl b hb fun x x_1 => limitRecOn x hm hs hl

Proof state:
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hm : (a : α) → IsMin a → C a
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccLimit a → ((b : α) → b < a → C b) → C a
hb : IsSuccLimit b
⊢ (hl b ⋯ fun x x_1 => prelimitRecOn x hs fun a ha IH => if h : IsMin a then hm a h else hl a ⋯ IH) =
    hl b hb fun x x_1 => limitRecOn x hm hs hl

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Indicator.lean
lemma indicator_mul_left (s : Set ι) (f g : ι → M₀) :
    indicator s (fun j ↦ f j * g j) i = indicator s f i * g i

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
⊢ s.indicator (fun j => f j * g j) i = s.indicator f i * g i

Tactic:
simp only [indicator]

Result:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
⊢ (if i ∈ s then f i * g i else 0) = (if i ∈ s then f i else 0) * g i

Proof state:
case pos
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h✝ : i ∈ s
⊢ f i * g i = f i * g i

Tactic:
rfl

Result:
no goals

Proof state:
case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h✝ : i ∉ s
⊢ 0 = 0 * g i

Tactic:
rw [zero_mul]

Result:
no goals

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
⊢ (if i ∈ s then f i * g i else 0) = (if i ∈ s then f i else 0) * g i

Tactic:
split_ifs

Result:
case pos
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h✝ : i ∈ s
⊢ f i * g i = f i * g i

case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h✝ : i ∉ s
⊢ 0 = 0 * g i
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem derivBFamily_fp {i hi} (H : IsNormal (f i hi)) (a : Ordinal) :
    f i hi (derivBFamily.{u, v} o f a) = derivBFamily.{u, v} o f a

Proof state:
case H
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ IsNormal (f i ?H.hi)

case H.hi
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ i < o

Tactic:
exact H

Result:
no goals

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ f i hi (o.derivBFamily f a) = o.derivBFamily f a

Tactic:
rw [← familyOfBFamily_enum o f]

Result:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ o.familyOfBFamily f ((enum fun x1 x2 => x1 < x2) ⟨i, ⋯⟩) (o.derivBFamily f a) = o.derivBFamily f a

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ o.familyOfBFamily f ((enum fun x1 x2 => x1 < x2) ⟨i, ⋯⟩) (o.derivBFamily f a) = o.derivBFamily f a

Tactic:
apply derivFamily_fp

Result:
case H
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ IsNormal (o.familyOfBFamily f ((enum fun x1 x2 => x1 < x2) ⟨i, ⋯⟩))

Proof state:
case H
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ IsNormal (o.familyOfBFamily f ((enum fun x1 x2 => x1 < x2) ⟨i, ⋯⟩))

Tactic:
rw [familyOfBFamily_enum]

Result:
case H
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ IsNormal (f i ?H.hi)

case H.hi
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ i < o
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKeyD_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a fallback : α}
    (hl : DistinctKeys l) (h : Perm l l') :
    getKeyD a l fallback = getKeyD a l' fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
a fallback : α
hl : DistinctKeys l
h : l.Perm l'
⊢ getKeyD a l fallback = getKeyD a l' fallback

Tactic:
simp only [getKeyD_eq_getKey?, getKey?_of_perm hl h]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Monoidal.lean
@[ext (iff := false)]
lemma tensorObj₄_ext {j : I} {A : C} (f g : tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j ⟶ A)
    [HasGoodTensorTensor₂₃ X₂ X₃ X₄]
    [H : HasTensor₄ObjExt X₁ X₂ X₃ X₄]
    (h : ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j),
      ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f =
        ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g) : f = g

Proof state:
case h.h
I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝³ : X₃.HasTensor X₄
inst✝² : X₂.HasTensor (tensorObj X₃ X₄)
inst✝¹ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
j : I
A : C
f g : tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j ⟶ A
inst✝ : X₂.HasGoodTensorTensor₂₃ X₃ X₄
H : X₁.HasTensor₄ObjExt X₂ X₃ X₄
h :
  ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j),
    ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g
i₁ i₂₃₄ : I
h' : i₁ + i₂₃₄ = j
i₂ i₃ i₄ : I
h'' : i₂ + i₃ + i₄ = i₂₃₄
⊢ X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ h'' ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ f =
    X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ h'' ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ g

Tactic:
have hj : i₁ + i₂ + i₃ + i₄ = j := by simp only [← h', ← h'', add_assoc]

Result:
case h.h
I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝³ : X₃.HasTensor X₄
inst✝² : X₂.HasTensor (tensorObj X₃ X₄)
inst✝¹ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
j : I
A : C
f g : tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j ⟶ A
inst✝ : X₂.HasGoodTensorTensor₂₃ X₃ X₄
H : X₁.HasTensor₄ObjExt X₂ X₃ X₄
h :
  ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j),
    ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g
i₁ i₂₃₄ : I
h' : i₁ + i₂₃₄ = j
i₂ i₃ i₄ : I
h'' : i₂ + i₃ + i₄ = i₂₃₄
hj : i₁ + i₂ + i₃ + i₄ = j
⊢ X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ h'' ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ f =
    X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ h'' ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ g

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₃ X₄ : GradedObject I C
inst✝³ : X₃.HasTensor X₄
inst✝² : X₂.HasTensor (tensorObj X₃ X₄)
inst✝¹ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
j : I
A : C
f g : tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j ⟶ A
inst✝ : X₂.HasGoodTensorTensor₂₃ X₃ X₄
H : X₁.HasTensor₄ObjExt X₂ X₃ X₄
h :
  ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j),
    ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g
i₁ i₂₃₄ : I
h' : i₁ + i₂₃₄ = j
i₂ i₃ i₄ : I
h'' : i₂ + i₃ + i₄ = i₂₃₄
⊢ i₁ + i₂ + i₃ + i₄ = j

Tactic:
simp only [← h', ← h'', add_assoc]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem j_ne_zero_of_isCharTwoJNeZeroNF_of_char_two : W.j ≠ 0

Proof state:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP F 2
⊢ W.j ≠ 0

Tactic:
rw [j_of_isCharTwoJNeZeroNF_of_char_two, div_ne_zero_iff]

Result:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP F 2
⊢ 1 ≠ 0 ∧ W.a₆ ≠ 0

Proof state:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP F 2
h : W.a₆ ≠ 0
⊢ 1 ≠ 0 ∧ W.a₆ ≠ 0

Tactic:
exact ⟨one_ne_zero, h⟩

Result:
no goals

Proof state:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP F 2
h : ↑W.Δ' ≠ 0
⊢ 1 ≠ 0 ∧ W.a₆ ≠ 0

Tactic:
rw [coe_Δ', Δ_of_isCharTwoJNeZeroNF_of_char_two] at h

Result:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP F 2
h : W.a₆ ≠ 0
⊢ 1 ≠ 0 ∧ W.a₆ ≠ 0

Proof state:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP F 2
⊢ 1 ≠ 0 ∧ W.a₆ ≠ 0

Tactic:
have h := W.Δ'.ne_zero

Result:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP F 2
h : ↑W.Δ' ≠ 0
⊢ 1 ≠ 0 ∧ W.a₆ ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem any_toArray (p : α → Bool) (v : Vector α n) :
    v.toArray.any p = v.any p

Proof state:
α : Type u_1
n : Nat
p : α → Bool
v : Vector α n
⊢ v.any p = v.any p

Tactic:
cases v

Result:
case mk
α : Type u_1
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.any p =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.any p

Proof state:
case mk
α : Type u_1
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.any p =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.any p

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem Subsingleton.nodup {s : Cycle α} (h : Subsingleton s) : Nodup s

Proof state:
case h.cons
α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))

Tactic:
have : tl = [] := by simpa [Subsingleton, length_eq_zero, Nat.succ_le_succ_iff] using h

Result:
case h.cons
α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
this : tl = []
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))

Proof state:
case h.nil
α : Type u_1
h : Subsingleton (Quot.mk ⇑(IsRotated.setoid α) [])
⊢ Nodup (Quot.mk ⇑(IsRotated.setoid α) [])

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s : Cycle α
h : s.Subsingleton
⊢ s.Nodup

Tactic:
induction' s using Quot.inductionOn with l

Result:
case h
α : Type u_1
l : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) l)
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α)) l)

Proof state:
case h
α : Type u_1
l : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) l)
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α)) l)

Tactic:
obtain - | ⟨hd, tl⟩ := l

Result:
case h.nil
α : Type u_1
h : Subsingleton (Quot.mk ⇑(IsRotated.setoid α) [])
⊢ Nodup (Quot.mk ⇑(IsRotated.setoid α) [])

case h.cons
α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))

Proof state:
case h.cons
α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
this : tl = []
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))

Tactic:
simp [this]

Result:
no goals

Proof state:
α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
⊢ tl = []

Tactic:
simpa [Subsingleton, length_eq_zero, Nat.succ_le_succ_iff] using h

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem induction_on {motive : (⨂[R] i, s i) → Prop} (z : ⨂[R] i, s i)
    (smul_tprod : ∀ (r : R) (f : Π i, s i), motive (r • tprod R f))
    (add : ∀ x y, motive x → motive y → motive (x + y)) :
    motive z

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
motive : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
smul_tprod : ∀ (r : R) (f : (i : ι) → s i), motive (r • (tprod R) f)
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
⊢ motive z

Tactic:
simp_rw [← tprodCoeff_eq_smul_tprod] at smul_tprod

Result:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
motive : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
smul_tprod : ∀ (r : R) (f : (i : ι) → s i), motive (tprodCoeff R r f)
⊢ motive z

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
motive : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
smul_tprod : ∀ (r : R) (f : (i : ι) → s i), motive (tprodCoeff R r f)
⊢ motive z

Tactic:
exact PiTensorProduct.induction_on' z smul_tprod add

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma abs_le_of_sq_le_sq (h : a ^ 2 ≤ b ^ 2) (hb : 0 ≤ b) : |a| ≤ b

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
h : a ^ 2 ≤ b ^ 2
hb : 0 ≤ b
⊢ |a| ≤ b

Tactic:
rwa [← abs_of_nonneg hb, ← sq_le_sq]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
lemma accumulate_last {i n m : ℕ} (hin : i < n) (hmi : m = i + 1) (t : Fin n → ℕ)
    (ht : ∀ j : Fin n, m ≤ j → t j = 0) :
    accumulate n m t ⟨i, i.lt_succ_self.trans_eq hmi.symm⟩ = t ⟨i, hin⟩

Proof state:
case h₀
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
j : Fin n
hji : j ≠ ⟨i, hin⟩
hij : i ≤ ↑j
⊢ m ≤ ↑j

Tactic:
exact hmi.trans_le (hij.lt_of_ne (Fin.val_ne_iff.2 hji).symm).nat_succ_le

Result:
no goals

Proof state:
case h₀
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
j : Fin n
hij : j ∈ filter (fun i_1 => ↑⟨i, ⋯⟩ ≤ ↑i_1) univ
hji : j ≠ ⟨i, hin⟩
⊢ m ≤ ↑j

Tactic:
simp_rw [mem_filter, mem_univ, true_and] at hij

Result:
case h₀
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
j : Fin n
hji : j ≠ ⟨i, hin⟩
hij : i ≤ ↑j
⊢ m ≤ ↑j

Proof state:
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
⊢ (accumulate n m) t ⟨i, ⋯⟩ = t ⟨i, hin⟩

Tactic:
rw [accumulate_apply]

Result:
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
⊢ ∑ i ∈ filter (fun i_1 => ↑⟨i, ⋯⟩ ≤ ↑i_1) univ, t i = t ⟨i, hin⟩

Proof state:
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
⊢ ∑ i ∈ filter (fun i_1 => ↑⟨i, ⋯⟩ ≤ ↑i_1) univ, t i = t ⟨i, hin⟩

Tactic:
apply sum_eq_single_of_mem

Result:
case h
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
⊢ ⟨i, hin⟩ ∈ filter (fun i_1 => ↑⟨i, ⋯⟩ ≤ ↑i_1) univ

case h₀
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
⊢ ∀ b ∈ filter (fun i_1 => ↑⟨i, ⋯⟩ ≤ ↑i_1) univ, b ≠ ⟨i, hin⟩ → t b = 0

Proof state:
case h
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
⊢ ⟨i, hin⟩ ∈ univ ∧ ↑⟨i, ⋯⟩ ≤ ↑⟨i, hin⟩

Tactic:
exact ⟨mem_univ _, le_rfl⟩

Result:
no goals

Proof state:
case h
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
⊢ ⟨i, hin⟩ ∈ filter (fun i_1 => ↑⟨i, ⋯⟩ ≤ ↑i_1) univ

Tactic:
rw [mem_filter]

Result:
case h
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
⊢ ⟨i, hin⟩ ∈ univ ∧ ↑⟨i, ⋯⟩ ≤ ↑⟨i, hin⟩

Proof state:
case h₀
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
⊢ ∀ b ∈ filter (fun i_1 => ↑⟨i, ⋯⟩ ≤ ↑i_1) univ, b ≠ ⟨i, hin⟩ → t b = 0

Tactic:
refine fun j hij hji ↦ ht j ?_

Result:
case h₀
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
j : Fin n
hij : j ∈ filter (fun i_1 => ↑⟨i, ⋯⟩ ≤ ↑i_1) univ
hji : j ≠ ⟨i, hin⟩
⊢ m ≤ ↑j
-- Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean
@[to_additive]
lemma le_self_pow (ha : 1 ≤ a) (hn : n ≠ 0) : a ≤ a ^ n

Proof state:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
n : ℕ
ha : 1 ≤ a
hn : n ≠ 0
⊢ a ≤ a ^ n

Tactic:
simpa using pow_le_pow_right' ha (Nat.one_le_iff_ne_zero.2 hn)

Result:
no goals
-- Mathlib/Data/Rat/Floor.lean
theorem ceil_cast (x : ℚ) : ⌈(x : α)⌉ = ⌈x⌉

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
⊢ ⌈↑x⌉ = ⌈x⌉

Tactic:
rw [← neg_inj, ← floor_neg, ← floor_neg, ← Rat.cast_neg, Rat.floor_cast]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma fundCircuit_eq_of_not_mem_ground (heX : e ∉ M.E) : M.fundCircuit e X = {e}

Proof state:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
⊢ ∀ a ∈ X, (∀ t ⊆ X, M.closure ∅ ⊆ M.closure t → a ∈ t) → a = e

Tactic:
exact fun a haX h ↦ by simpa using h ∅ (empty_subset X) rfl.subset

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
⊢ M.fundCircuit e X = {e}

Tactic:
suffices h : ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e by
  simpa [subset_antisymm_iff, fundCircuit]

Result:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
⊢ ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e

Proof state:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
a : α
haX : a ∈ X
h : ∀ t ⊆ X, M.closure ∅ ⊆ M.closure t → a ∈ t
⊢ a = e

Tactic:
simpa using h ∅ (empty_subset X) rfl.subset

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
⊢ ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e

Tactic:
simp_rw [← M.closure_inter_ground {e}, singleton_inter_eq_empty.2 heX]

Result:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
⊢ ∀ a ∈ X, (∀ t ⊆ X, M.closure ∅ ⊆ M.closure t → a ∈ t) → a = e

Proof state:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
h : ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e
⊢ M.fundCircuit e X = {e}

Tactic:
simpa [subset_antisymm_iff, fundCircuit]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem smul_finset_subset_iff : a • s ⊆ t ↔ s ⊆ a⁻¹ • t

Proof state:
α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ a • ↑s ⊆ ↑t ↔ ↑s ⊆ a⁻¹ • ↑t

Tactic:
exact Set.smul_set_subset_iff_subset_inv_smul_set

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ a • s ⊆ t ↔ s ⊆ a⁻¹ • t

Tactic:
simp_rw [← coe_subset]

Result:
α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ ↑(a • s) ⊆ ↑t ↔ ↑s ⊆ ↑(a⁻¹ • t)

Proof state:
α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ ↑(a • s) ⊆ ↑t ↔ ↑s ⊆ ↑(a⁻¹ • t)

Tactic:
push_cast

Result:
α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ a • ↑s ⊆ ↑t ↔ ↑s ⊆ a⁻¹ • ↑t
-- Mathlib/Algebra/Module/Presentation/Basic.lean
lemma of_linearEquiv (e : M ≃ₗ[A] N) : (solution.postcomp e.toLinearMap).IsPresentation where
  bijective

Proof state:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
e : M ≃ₗ[A] N
⊢ Function.Bijective ⇑(solution.postcomp ↑e).fromQuotient

Tactic:
have : (solution.postcomp e.toLinearMap).fromQuotient =
  e.toLinearMap.comp (solution.fromQuotient) := by aesop

Result:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
e : M ≃ₗ[A] N
this : (solution.postcomp ↑e).fromQuotient = ↑e ∘ₗ solution.fromQuotient
⊢ Function.Bijective ⇑(solution.postcomp ↑e).fromQuotient

Proof state:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
e : M ≃ₗ[A] N
this : (solution.postcomp ↑e).fromQuotient = ↑e ∘ₗ solution.fromQuotient
⊢ Function.Bijective ⇑(solution.postcomp ↑e).fromQuotient

Tactic:
rw [this, LinearMap.coe_comp, LinearEquiv.coe_coe]

Result:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
e : M ≃ₗ[A] N
this : (solution.postcomp ↑e).fromQuotient = ↑e ∘ₗ solution.fromQuotient
⊢ Function.Bijective (⇑e ∘ ⇑solution.fromQuotient)

Proof state:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
e : M ≃ₗ[A] N
⊢ (solution.postcomp ↑e).fromQuotient = ↑e ∘ₗ solution.fromQuotient

Tactic:
aesop

Result:
no goals

Proof state:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
e : M ≃ₗ[A] N
this : (solution.postcomp ↑e).fromQuotient = ↑e ∘ₗ solution.fromQuotient
⊢ Function.Bijective (⇑e ∘ ⇑solution.fromQuotient)

Tactic:
exact Function.Bijective.comp e.bijective h.bijective

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.xor_right_inj (a b c : BitVec w) : (c ^^^ a == c ^^^ b) = (a == b)

Proof state:
w : Nat
a b c : BitVec w
⊢ (c ^^^ a == c ^^^ b) = (a == b)

Tactic:
rw [Bool.eq_iff_iff]

Result:
w : Nat
a b c : BitVec w
⊢ (c ^^^ a == c ^^^ b) = true ↔ (a == b) = true

Proof state:
w : Nat
a b c : BitVec w
⊢ (c ^^^ a == c ^^^ b) = true ↔ (a == b) = true

Tactic:
simp

Result:
no goals