harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/FiniteType.lean
theorem iff_quotient_freeAlgebra' : FiniteType R A ↔
    ∃ (ι : Type uA) (_ : Fintype ι) (f : FreeAlgebra R ι →ₐ[R] A), Surjective f

Proof state:
case mpr.intro.intro.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Type uA
hfintype : Fintype ι
f : FreeAlgebra R ι →ₐ[R] A
hsur : Surjective ⇑f
this : Fintype ι := hfintype
⊢ FiniteType R A

Tactic:
exact FiniteType.of_surjective (FiniteType.freeAlgebra R ι) f hsur

Result:
no goals

Proof state:
case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (∃ s f, Surjective ⇑f) → ∃ ι x f, Surjective ⇑f

Tactic:
rintro ⟨s, ⟨f, hsur⟩⟩

Result:
case mp.intro.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
f : FreeAlgebra R { x // x ∈ s } →ₐ[R] A
hsur : Surjective ⇑f
⊢ ∃ ι x f, Surjective ⇑f

Proof state:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ FiniteType R A ↔ ∃ ι x f, Surjective ⇑f

Tactic:
constructor

Result:
case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ FiniteType R A → ∃ ι x f, Surjective ⇑f

case mpr
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (∃ ι x f, Surjective ⇑f) → FiniteType R A

Proof state:
case mpr
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (∃ ι x f, Surjective ⇑f) → FiniteType R A

Tactic:
rintro ⟨ι, ⟨hfintype, ⟨f, hsur⟩⟩⟩

Result:
case mpr.intro.intro.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Type uA
hfintype : Fintype ι
f : FreeAlgebra R ι →ₐ[R] A
hsur : Surjective ⇑f
⊢ FiniteType R A

Proof state:
case mpr.intro.intro.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Type uA
hfintype : Fintype ι
f : FreeAlgebra R ι →ₐ[R] A
hsur : Surjective ⇑f
⊢ FiniteType R A

Tactic:
letI : Fintype ι := hfintype

Result:
case mpr.intro.intro.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Type uA
hfintype : Fintype ι
f : FreeAlgebra R ι →ₐ[R] A
hsur : Surjective ⇑f
this : Fintype ι := hfintype
⊢ FiniteType R A

Proof state:
case mp.intro.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
f : FreeAlgebra R { x // x ∈ s } →ₐ[R] A
hsur : Surjective ⇑f
⊢ ∃ ι x f, Surjective ⇑f

Tactic:
use { x : A // x ∈ s }, inferInstance, f

Result:
no goals

Proof state:
case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ FiniteType R A → ∃ ι x f, Surjective ⇑f

Tactic:
rw [iff_quotient_freeAlgebra]

Result:
case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (∃ s f, Surjective ⇑f) → ∃ ι x f, Surjective ⇑f
-- Mathlib/CategoryTheory/Endofunctor/Algebra.lean
theorem right_inv' :
    ⟨A.str ≫ strInv h, by rw [Category.assoc, F.map_comp, strInv, ← Hom.h] ⟩ = 𝟙 A :=
  Limits.IsTerminal.hom_ext h _ (𝟙 A)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
A : Coalgebra F
h : Limits.IsTerminal A
⊢ A.str ≫ F.map (A.str ≫ strInv h) = (A.str ≫ strInv h) ≫ A.str

Tactic:
rw [Category.assoc, F.map_comp, strInv, ← Hom.h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapIdx_eq_replicate_iff {l : List α} {f : Nat → α → β} {b : β} :
    mapIdx f l = replicate l.length b ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] = b

Proof state:
case mp
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
b : β
⊢ (∀ (b_1 : β) (x : Nat) (x_1 : x < l.length), f x l[x] = b_1 → b_1 = b) → ∀ (i : Nat) (h : i < l.length), f i l[i] = b

Tactic:
intro w i h

Result:
case mp
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
b : β
w : ∀ (b_1 : β) (x : Nat) (x_1 : x < l.length), f x l[x] = b_1 → b_1 = b
i : Nat
h : i < l.length
⊢ f i l[i] = b

Proof state:
case mpr
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
b : β
⊢ (∀ (i : Nat) (h : i < l.length), f i l[i] = b) → ∀ (b_1 : β) (x : Nat) (x_1 : x < l.length), f x l[x] = b_1 → b_1 = b

Tactic:
rintro w _ i h rfl

Result:
case mpr
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
b : β
w : ∀ (i : Nat) (h : i < l.length), f i l[i] = b
i : Nat
h : i < l.length
⊢ f i l[i] = b

Proof state:
case mp
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
b : β
w : ∀ (b_1 : β) (x : Nat) (x_1 : x < l.length), f x l[x] = b_1 → b_1 = b
i : Nat
h : i < l.length
⊢ f i l[i] = b

Tactic:
apply w _ _ _ rfl

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
b : β
w : ∀ (i : Nat) (h : i < l.length), f i l[i] = b
i : Nat
h : i < l.length
⊢ f i l[i] = b

Tactic:
exact w i h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
b : β
⊢ mapIdx f l = replicate l.length b ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] = b

Tactic:
simp only [eq_replicate_iff, length_mapIdx, mem_mapIdx, forall_exists_index, true_and]

Result:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
b : β
⊢ (∀ (b_1 : β) (x : Nat) (x_1 : x < l.length), f x l[x] = b_1 → b_1 = b) ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] = b

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
b : β
⊢ (∀ (b_1 : β) (x : Nat) (x_1 : x < l.length), f x l[x] = b_1 → b_1 = b) ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] = b

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
b : β
⊢ (∀ (b_1 : β) (x : Nat) (x_1 : x < l.length), f x l[x] = b_1 → b_1 = b) → ∀ (i : Nat) (h : i < l.length), f i l[i] = b

case mpr
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
b : β
⊢ (∀ (i : Nat) (h : i < l.length), f i l[i] = b) → ∀ (b_1 : β) (x : Nat) (x_1 : x < l.length), f x l[x] = b_1 → b_1 = b
-- Mathlib/Data/Fintype/Card.lean
theorem card_of_subtype {p : α → Prop} (s : Finset α) (H : ∀ x : α, x ∈ s ↔ p x)
    [Fintype { x // p x }] : card { x // p x } = #s

Proof state:
α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
inst✝ : Fintype { x // p x }
⊢ card { x // p x } = #s

Tactic:
rw [← subtype_card s H]

Result:
α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
inst✝ : Fintype { x // p x }
⊢ card { x // p x } = card { x // p x }

Proof state:
α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
inst✝ : Fintype { x // p x }
⊢ card { x // p x } = card { x // p x }

Tactic:
congr!

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup'_insert [DecidableEq β] {b : β} :
    (insert b s).sup' (insert_nonempty _ _) f = f b ⊔ s.sup' H f

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
inst✝ : DecidableEq β
b : β
⊢ ↑((insert b s).sup' ⋯ f) = ↑(f b ⊔ s.sup' H f)

Tactic:
simp [WithBot.coe_sup]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
inst✝ : DecidableEq β
b : β
⊢ (insert b s).sup' ⋯ f = f b ⊔ s.sup' H f

Tactic:
rw [← WithBot.coe_eq_coe]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
inst✝ : DecidableEq β
b : β
⊢ ↑((insert b s).sup' ⋯ f) = ↑(f b ⊔ s.sup' H f)
-- Mathlib/Algebra/Ring/Parity.lean
@[simp] lemma not_even_bit1 (n : ℕ) : ¬Even (2 * n + 1)

Proof state:
n : ℕ
⊢ ¬Even (2 * n + 1)

Tactic:
simp [parity_simps]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem ofReal_mul_pos_iff (x : ℝ) (z : K) :
    0 < x * z ↔ (x < 0 ∧ z < 0) ∨ (0 < x ∧ 0 < z)

Proof state:
K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
⊢ 0 < ↑x * z ↔ x < 0 ∧ z < 0 ∨ 0 < x ∧ 0 < z

Tactic:
simp only [pos_iff (K := K), neg_iff (K := K), re_ofReal_mul, im_ofReal_mul]

Result:
K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
⊢ 0 < x * re z ∧ x * im z = 0 ↔ x < 0 ∧ re z < 0 ∧ im z = 0 ∨ 0 < x ∧ 0 < re z ∧ im z = 0

Proof state:
K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
⊢ 0 < x * re z ∧ x * im z = 0 ↔ x < 0 ∧ re z < 0 ∧ im z = 0 ∨ 0 < x ∧ 0 < re z ∧ im z = 0

Tactic:
obtain hx | hx | hx := lt_trichotomy x 0

Result:
case inl
K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
hx : x < 0
⊢ 0 < x * re z ∧ x * im z = 0 ↔ x < 0 ∧ re z < 0 ∧ im z = 0 ∨ 0 < x ∧ 0 < re z ∧ im z = 0

case inr.inl
K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
hx : x = 0
⊢ 0 < x * re z ∧ x * im z = 0 ↔ x < 0 ∧ re z < 0 ∧ im z = 0 ∨ 0 < x ∧ 0 < re z ∧ im z = 0

case inr.inr
K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
hx : 0 < x
⊢ 0 < x * re z ∧ x * im z = 0 ↔ x < 0 ∧ re z < 0 ∧ im z = 0 ∨ 0 < x ∧ 0 < re z ∧ im z = 0

Proof state:
case inr.inr
K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
hx : 0 < x
⊢ 0 < x * re z ∧ x * im z = 0 ↔ x < 0 ∧ re z < 0 ∧ im z = 0 ∨ 0 < x ∧ 0 < re z ∧ im z = 0

Tactic:
simp only [mul_pos_iff, hx, true_and, not_lt_of_gt hx, false_and, or_false, mul_eq_zero,
  hx.ne', false_or]

Result:
no goals

Proof state:
case inr.inl
K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
hx : x = 0
⊢ 0 < x * re z ∧ x * im z = 0 ↔ x < 0 ∧ re z < 0 ∧ im z = 0 ∨ 0 < x ∧ 0 < re z ∧ im z = 0

Tactic:
simp only [hx, zero_mul, lt_self_iff_false, false_and, false_or]

Result:
no goals

Proof state:
case inl
K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
hx : x < 0
⊢ 0 < x * re z ∧ x * im z = 0 ↔ x < 0 ∧ re z < 0 ∧ im z = 0 ∨ 0 < x ∧ 0 < re z ∧ im z = 0

Tactic:
simp only [mul_pos_iff, not_lt_of_gt hx, false_and, hx, true_and, false_or, mul_eq_zero, hx.ne,
  or_false]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem preimage_const (b : β) (s : Set β) [Decidable (b ∈ s)] :
    (fun _ : α => b) ⁻¹' s = if b ∈ s then univ else ∅

Proof state:
case pos
α : Type u_1
β : Type u_2
b : β
s : Set β
inst✝ : Decidable (b ∈ s)
hb : b ∈ s
⊢ (fun x => b) ⁻¹' s = univ

case neg
α : Type u_1
β : Type u_2
b : β
s : Set β
inst✝ : Decidable (b ∈ s)
hb : b ∉ s
⊢ (fun x => b) ⁻¹' s = ∅

Tactic:
exacts [preimage_const_of_mem hb, preimage_const_of_not_mem hb]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
b : β
s : Set β
inst✝ : Decidable (b ∈ s)
⊢ (fun x => b) ⁻¹' s = if b ∈ s then univ else ∅

Tactic:
split_ifs with hb

Result:
case pos
α : Type u_1
β : Type u_2
b : β
s : Set β
inst✝ : Decidable (b ∈ s)
hb : b ∈ s
⊢ (fun x => b) ⁻¹' s = univ

case neg
α : Type u_1
β : Type u_2
b : β
s : Set β
inst✝ : Decidable (b ∈ s)
hb : b ∉ s
⊢ (fun x => b) ⁻¹' s = ∅
-- Mathlib/Analysis/Normed/Group/AddTorsor.lean
theorem nndist_vsub_vsub_le (p₁ p₂ p₃ p₄ : P) :
    nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄

Proof state:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
⊢ nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄

Tactic:
simp only [← NNReal.coe_le_coe, NNReal.coe_add, ← dist_nndist, dist_vsub_vsub_le]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
lemma isIso_inr_of_isIso (h : IsPushout f g inl inr) [IsIso f] : IsIso inr

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : IsIso f
⊢ IsIso inr

Tactic:
have := h.hasPushout

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : IsIso f
this : HasPushout f g
⊢ IsIso inr

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : IsIso f
this : HasPushout f g
⊢ IsIso (pushout.inr f g ≫ h.isoPushout.inv)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : IsIso f
this : HasPushout f g
⊢ IsIso inr

Tactic:
rw [← h.inr_isoPushout_inv]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : IsIso f
this : HasPushout f g
⊢ IsIso (pushout.inr f g ≫ h.isoPushout.inv)
-- Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean
lemma eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero {x : M}
    (hx : x ∈ P.rootSpan) (hx' : P.RootForm x x = 0) :
    x = 0

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : LinearOrderedCommRing R
inst✝¹ : Module R M
inst✝ : Module R N
P : RootPairing ι R M N
x : M
hx : x ∈ P.rootSpan
hx' : (P.RootForm x) x = 0
this : x ∈ P.rootSpan ⊓ LinearMap.ker P.RootForm
⊢ x = 0

Tactic:
simpa [P.disjoint_rootSpan_ker_rootForm.eq_bot] using this

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : LinearOrderedCommRing R
inst✝¹ : Module R M
inst✝ : Module R N
P : RootPairing ι R M N
x : M
hx : x ∈ P.rootSpan
hx' : (P.RootForm x) x = 0
⊢ x = 0

Tactic:
have : x ∈ P.rootSpan ⊓ LinearMap.ker P.RootForm := ⟨hx, P.rootForm_self_eq_zero_iff.mp hx'⟩

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : LinearOrderedCommRing R
inst✝¹ : Module R M
inst✝ : Module R N
P : RootPairing ι R M N
x : M
hx : x ∈ P.rootSpan
hx' : (P.RootForm x) x = 0
this : x ∈ P.rootSpan ⊓ LinearMap.ker P.RootForm
⊢ x = 0
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem integrable_finset_sum_measure {ι} {m : MeasurableSpace α} {f : α → β} {μ : ι → Measure α}
    {s : Finset ι} : Integrable f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
ι : Type u_6
m : MeasurableSpace α
f : α → β
μ : ι → Measure α
s : Finset ι
⊢ Integrable f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)

Tactic:
induction s using Finset.induction_on <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
ι : Type u_6
m : MeasurableSpace α
f : α → β
μ : ι → Measure α
s : Finset ι
⊢ Integrable f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)

Tactic:
classical
induction s using Finset.induction_on <;> simp [*]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem LiftRel.swap_lem {R : α → β → Prop} {s1 s2} (h : LiftRel R s1 s2) :
    LiftRel (swap R) s2 s1

Proof state:
α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h✝ : LiftRel R s1 s2
s : WSeq β
t : WSeq α
h : LiftRel R t s
⊢ Computation.LiftRel (LiftRelO (swap R) (swap (LiftRel R))) s.destruct t.destruct

Tactic:
rw [← LiftRelO.swap, Computation.LiftRel.swap]

Result:
α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h✝ : LiftRel R s1 s2
s : WSeq β
t : WSeq α
h : LiftRel R t s
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct s.destruct

Proof state:
α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h : LiftRel R s1 s2
⊢ LiftRel (swap R) s2 s1

Tactic:
refine ⟨swap (LiftRel R), h, fun {s t} (h : LiftRel R t s) => ?_⟩

Result:
α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h✝ : LiftRel R s1 s2
s : WSeq β
t : WSeq α
h : LiftRel R t s
⊢ Computation.LiftRel (LiftRelO (swap R) (swap (LiftRel R))) s.destruct t.destruct

Proof state:
α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h✝ : LiftRel R s1 s2
s : WSeq β
t : WSeq α
h : LiftRel R t s
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct s.destruct

Tactic:
apply liftRel_destruct h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem foldr_attachWith
    (l : List α) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : { x // q x} → β → β} {b} :
    (l.attachWith q H).foldr f b = l.attach.foldr (fun a acc => f ⟨a.1, H _ a.2⟩ acc) b

Proof state:
case cons
α : Type u_1
β : Type u_2
q : α → Prop
f : { x // q x } → β → β
a : α
l : List α
ih :
  ∀ (H : ∀ (a : α), a ∈ l → q a) {b : β},
    foldr f b (l.attachWith q H) = foldr (fun a acc => f ⟨a.val, ⋯⟩ acc) b l.attach
H : ∀ (a_1 : α), a_1 ∈ a :: l → q a_1
b : β
⊢ foldr f b ((a :: l).attachWith q H) = foldr (fun a_1 acc => f ⟨a_1.val, ⋯⟩ acc) b (a :: l).attach

Tactic:
simp [ih, foldr_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
q : α → Prop
H : ∀ (a : α), a ∈ l → q a
f : { x // q x } → β → β
b : β
⊢ foldr f b (l.attachWith q H) = foldr (fun a acc => f ⟨a.val, ⋯⟩ acc) b l.attach

Tactic:
induction l generalizing b with
| nil => simp
| cons a l ih => simp [ih, foldr_map]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
q : α → Prop
f : { x // q x } → β → β
H : ∀ (a : α), a ∈ [] → q a
b : β
⊢ foldr f b ([].attachWith q H) = foldr (fun a acc => f ⟨a.val, ⋯⟩ acc) b [].attach

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem exp_nsmul (n : ℕ) (x : 𝔸) : exp 𝕂 (n • x) = exp 𝕂 x ^ n

Proof state:
case zero
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
⊢ exp 𝕂 (0 • x) = exp 𝕂 x ^ 0

Tactic:
rw [zero_smul, pow_zero, exp_zero]

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
n : ℕ
x : 𝔸
⊢ exp 𝕂 (n • x) = exp 𝕂 x ^ n

Tactic:
induction n with
| zero => rw [zero_smul, pow_zero, exp_zero]
| succ n ih => rw [succ_nsmul, pow_succ, exp_add_of_commute ((Commute.refl x).smul_left n), ih]

Result:
no goals

Proof state:
case succ
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
ih : exp 𝕂 (n • x) = exp 𝕂 x ^ n
⊢ exp 𝕂 ((n + 1) • x) = exp 𝕂 x ^ (n + 1)

Tactic:
rw [succ_nsmul, pow_succ, exp_add_of_commute ((Commute.refl x).smul_left n), ih]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem out_snd_mem (e : Sym2 α) : e.out.2 ∈ e :=
  ⟨e.out.1, by rw [eq_swap, Sym2.mk, e.out_eq]⟩

Proof state:
α : Type u_1
e : Sym2 α
⊢ e = s((Quot.out e).2, (Quot.out e).1)

Tactic:
rw [eq_swap, Sym2.mk, e.out_eq]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem bind_ret (f : α → β) (s) : bind s (ret ∘ f) ~ʷ map f s

Proof state:
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ s.bind (ret ∘ f) ~ʷ map f s

Tactic:
dsimp [bind]

Result:
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ (map (ret ∘ f) s).join ~ʷ map f s

Proof state:
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ (map ret (map f s)).join ~ʷ map f s

Tactic:
apply join_map_ret

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ (map (ret ∘ f) s).join ~ʷ map f s

Tactic:
rw [map_comp]

Result:
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ (map ret (map f s)).join ~ʷ map f s
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem range_comp_of_range_eq_top [RingHomSurjective τ₁₂] [RingHomSurjective τ₂₃]
    [RingHomSurjective τ₁₃] {f : M →ₛₗ[τ₁₂] M₂} (g : M₂ →ₛₗ[τ₂₃] M₃) (hf : range f = ⊤) :
    range (g.comp f : M →ₛₗ[τ₁₃] M₃) = range g

Proof state:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹² : Semiring R
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring R₃
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : Module R M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝³ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst✝² : RingHomSurjective τ₁₂
inst✝¹ : RingHomSurjective τ₂₃
inst✝ : RingHomSurjective τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : range f = ⊤
⊢ range (g.comp f) = range g

Tactic:
rw [range_comp, hf, Submodule.map_top]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/EulerIdentity.lean
theorem IsHomogeneous.sum_X_mul_pderiv (h : φ.IsHomogeneous n) :
    ∑ i : σ, X i * pderiv i φ = n • φ

Proof state:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
h : φ.IsHomogeneous n
⊢ ∑ i : σ, X i * (pderiv i) φ = n • φ

Tactic:
simp_rw [← h.sum_weight_X_mul_pderiv, Pi.one_apply, one_smul]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma b₄_of_char_three : W.b₄ = -W.a₄ + W.a₁ * W.a₃

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ 2 * W.a₄ + W.a₁ * W.a₃ = -W.a₄ + W.a₁ * W.a₃

Tactic:
linear_combination W.a₄ * CharP.cast_eq_zero R 3

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.b₄ = -W.a₄ + W.a₁ * W.a₃

Tactic:
rw [b₄]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ 2 * W.a₄ + W.a₁ * W.a₃ = -W.a₄ + W.a₁ * W.a₃
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem pullback_singleton [HasPullbacks C] (g : Z ⟶ X) :
    pullbackArrows f (singleton g) = singleton (pullback.snd g f)

Proof state:
case h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
h : W ⟶ Y
⊢ h ∈ pullbackArrows f (singleton g) ↔ h ∈ singleton (pullback.snd g f)

Tactic:
constructor

Result:
case h.h.mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
h : W ⟶ Y
⊢ h ∈ pullbackArrows f (singleton g) → h ∈ singleton (pullback.snd g f)

case h.h.mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
h : W ⟶ Y
⊢ h ∈ singleton (pullback.snd g f) → h ∈ pullbackArrows f (singleton g)

Proof state:
case h.h.mp.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝¹ Z : C
f : Y✝¹ ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
Y✝ Y : C
⊢ pullback.snd g f ∈ singleton (pullback.snd g f)

Tactic:
exact singleton.mk

Result:
no goals

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
⊢ pullbackArrows f (singleton g) = singleton (pullback.snd g f)

Tactic:
ext h

Result:
case h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
h : W ⟶ Y
⊢ h ∈ pullbackArrows f (singleton g) ↔ h ∈ singleton (pullback.snd g f)

Proof state:
case h.h.mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
h : W ⟶ Y
⊢ h ∈ pullbackArrows f (singleton g) → h ∈ singleton (pullback.snd g f)

Tactic:
rintro ⟨W, _, _, _⟩

Result:
case h.h.mp.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝¹ Z : C
f : Y✝¹ ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
Y✝ Y : C
⊢ pullback.snd g f ∈ singleton (pullback.snd g f)

Proof state:
case h.h.mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
h : W ⟶ Y
⊢ h ∈ singleton (pullback.snd g f) → h ∈ pullbackArrows f (singleton g)

Tactic:
rintro ⟨_⟩

Result:
case h.h.mpr.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ Z : C
f : Y✝ ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
Y : C
⊢ pullback.snd g f ∈ pullbackArrows f (singleton g)

Proof state:
case h.h.mpr.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ Z : C
f : Y✝ ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
Y : C
⊢ pullback.snd g f ∈ pullbackArrows f (singleton g)

Tactic:
exact pullbackArrows.mk Z g singleton.mk

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
⊢ pullbackArrows f (singleton g) = singleton (pullback.snd g f)

Tactic:
funext W

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
⊢ pullbackArrows f (singleton g) = singleton (pullback.snd g f)