mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type v
⊢ ∀ {α β : Type v} (x : Comp F G α) (y : Comp F G β), x <* y = const β <$> x <*> y

Tactic:
intros

Goal state after:
F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ α✝ β✝ : Type v
x✝ : Comp F G α✝
y✝ : Comp F G β✝
⊢ x✝ <* y✝ = const β✝ <$> x✝ <*> y✝
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type v
⊢ ∀ {α β : Type v} (x : Comp F G α) (y : Comp F G β), x *> y = const α id <$> x <*> y

Tactic:
intros

Goal state after:
F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ α✝ β✝ : Type v
x✝ : Comp F G α✝
y✝ : Comp F G β✝
⊢ x✝ *> y✝ = const α✝ id <$> x✝ <*> y✝
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.reverse.get 0 = v.last

Tactic:
last_def,

Goal state after:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.reverse.get 0 = v.get (Fin.last n)
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
⊢ encode (decode (Sum.inr s)) = Sum.inr s

Tactic:
unfold SymOptionSuccEquiv.encode

Goal state after:
case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
⊢ (if h : none ∈ decode (Sum.inr s) then Sum.inl ((decode (Sum.inr s)).erase none h)
    else Sum.inr (map (fun o ↦ (↑o).get ⋯) (decode (Sum.inr s)).attach)) =
    Sum.inr s
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case cons
n : ℕ
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
ih : Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) w✝ = Comp.mk (Vector.traverse f <$> Vector.traverse g w✝)
⊢ Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) (x✝ ::ᵥ w✝) =
    Comp.mk (Vector.traverse f <$> Vector.traverse g (x✝ ::ᵥ w✝))

Tactic:
Vector.traverse_def,

Goal state after:
case cons
n : ℕ
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
ih : Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) w✝ = Comp.mk (Vector.traverse f <$> Vector.traverse g w✝)
⊢ cons <$> (Comp.mk ∘ Functor.map f ∘ g) x✝ <*> Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) w✝ =
    Comp.mk (Vector.traverse f <$> Vector.traverse g (x✝ ::ᵥ w✝))
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case cons
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
ih : (fun {α} ↦ η.app α) (Vector.traverse f w✝) = Vector.traverse ((fun {α} ↦ η.app α) ∘ f) w✝
⊢ (fun {α} ↦ η.app α) (Vector.traverse f (x✝ ::ᵥ w✝)) = Vector.traverse ((fun {α} ↦ η.app α) ∘ f) (x✝ ::ᵥ w✝)

Tactic:
Vector.traverse_def,

Goal state after:
case cons
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
ih : (fun {α} ↦ η.app α) (Vector.traverse f w✝) = Vector.traverse ((fun {α} ↦ η.app α) ∘ f) w✝
⊢ (fun {α} ↦ η.app α) (cons <$> f x✝ <*> Vector.traverse f w✝) = Vector.traverse ((fun {α} ↦ η.app α) ∘ f) (x✝ ::ᵥ w✝)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case cons
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
ih : (fun {α} ↦ η.app α) (Vector.traverse f w✝) = Vector.traverse ((fun {α} ↦ η.app α) ∘ f) w✝
⊢ (fun {α} ↦ η.app α) (cons <$> f x✝ <*> Vector.traverse f w✝) = Vector.traverse ((fun {α} ↦ η.app α) ∘ f) (x✝ ::ᵥ w✝)

Tactic:
Vector.traverse_def,

Goal state after:
case cons
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
ih : (fun {α} ↦ η.app α) (Vector.traverse f w✝) = Vector.traverse ((fun {α} ↦ η.app α) ∘ f) w✝
⊢ (fun {α} ↦ η.app α) (cons <$> f x✝ <*> Vector.traverse f w✝) =
    cons <$> ((fun {α} ↦ η.app α) ∘ f) x✝ <*> Vector.traverse ((fun {α} ↦ η.app α) ∘ f) w✝
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : x ≤ y
⊢ (sumLexIioIci x).symm y = toLex (Sum.inr ⟨y, h⟩)

Tactic:
rw [symm_apply_eq, sumLexIioIci_apply_inr]

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
c : β
ha : inl a < inr c
hb : inr c < inl b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
· exact (not_inl_lt_inr ha).elim

Goal state after:
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Goal state after:
case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
hlim : ¬IsSuccPrelimit (sSup ∅)
⊢ sSup ∅ ∈ ∅

case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
hs : s.Nonempty
⊢ sSup s ∈ s
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
r : α → α → Prop
β : Type u
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
⊢ ∃ γ t, IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)

Tactic:
by
  classical
  obtain f | f := f.principalSumRelIso
  · exact ⟨_, _, inferInstance,
      ⟨(RelIso.sumLexCongr f.subrelIso.symm (.refl _)).trans <| .sumLexComplLeft ..⟩⟩
  · exact ⟨PEmpty, nofun, inferInstance, ⟨(RelIso.sumLexEmpty r _).trans f⟩⟩

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : ScottContinuous f
hg : ScottContinuous g
⊢ ScottContinuous (g ∘ f)

Tactic:
← scottContinuousOn_univ

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : ScottContinuousOn univ f
hg : ScottContinuousOn univ g
⊢ ScottContinuousOn univ (g ∘ f)
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : α → γ
hf : ScottContinuous f
hg : ScottContinuous g
⊢ ScottContinuous fun x ↦ (f x, g x)

Tactic:
← scottContinuousOn_univ

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : α → γ
hf : ScottContinuousOn univ f
hg : ScottContinuousOn univ g
⊢ ScottContinuousOn univ fun x ↦ (f x, g x)
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ o.toOption = Option.some a ↔ a ∈ o

Tactic:
rw [← Option.mem_def, mem_toOption]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
b : β
x : Part α
f : α → Part β
⊢ x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b

Tactic:
simp only [eq_some_iff, mem_bind_iff]

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
⊢ ωSup c ≤ x → ∀ (i : ℕ), c i ≤ x

Tactic:
intros

Goal state after:
case mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ c i✝ ≤ x
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
⊢ (∀ (i : ℕ), c i ≤ x) → ωSup c ≤ x

Tactic:
intros

Goal state after:
case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ∀ (i : ℕ), c i ≤ x
⊢ ωSup c ≤ x
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ∀ (i : ℕ), c i ≤ x
⊢ ωSup c ≤ x

Tactic:
exact ωSup_le _ _ ‹_›

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Append α
a b : Part α
hab : (a ++ b).Dom
⊢ (a ++ b).get hab = a.get ⋯ ++ b.get ⋯

Tactic:
by
  simp [append_def]; aesop

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: c c' : Cardinal.{u_1}
| #(Quotient.out c) ≤ #(Quotient.out c')

Tactic:
le_def

Goal state after:
c c' : Cardinal.{u_1}
| Nonempty (Quotient.out c ↪ Quotient.out c')
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case refine_1
α β : Type u
a b : Cardinal.{u}
x✝¹ x✝ : Type u
⊢ Nonempty (x✝¹ ↪ x✝) ↔ #x✝¹ ≤ #x✝

Tactic:
le_def

Goal state after:
case refine_1
α β : Type u
a b : Cardinal.{u}
x✝¹ x✝ : Type u
⊢ Nonempty (x✝¹ ↪ x✝) ↔ Nonempty (x✝¹ ↪ x✝)
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsStrongLimit
⊢ IsSuccLimit c

Tactic:
Cardinal.isSuccLimit_iff

Goal state after:
c : Cardinal.{u_1}
hc : c.IsStrongLimit
⊢ c ≠ 0 ∧ IsSuccPrelimit c
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ⊢ IsSuccLimit ℵ₀

Tactic:
Cardinal.isSuccLimit_iff

Goal state after:
⊢ ℵ₀ ≠ 0 ∧ IsSuccPrelimit ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
s : Set α
a : α
h : a ∉ s
⊢ #↑(insert a s) = #↑s + 1

Tactic:
rw [← union_singleton, mk_union_of_disjoint, mk_singleton]
  simpa

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mp
α : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃! y, y ≠ x

Tactic:
rintro ⟨a, b, hne, h⟩
    simp only [eq_univ_iff_forall, mem_insert_iff, mem_singleton_iff] at h
    rcases h x with (rfl | rfl)
    exacts [⟨b, hne.symm, fun z => (h z).resolve_left⟩, ⟨a, hne, fun z => (h z).resolve_right⟩]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b c : Cardinal.{u}
⊢ a ^< b ≤ c ↔ ∀ x < b, a ^ x ≤ c

Tactic:
by
  rw [powerlt, ciSup_le_iff']
  · simp
  · rw [← image_eq_range]
    exact bddAbove_image.{u, u} _ bddAbove_Iio

Goal state after:
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁶ : CommSemiring R✝
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
inst✝² : Semiring B
inst✝¹ : Algebra R✝ B
R : Type ?u.22
A : Type ?u.24
x✝² : CommSemiring R
x✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : A
⊢ 1 • x✝ = x✝

Tactic:
by simp [smul_def']

Goal state after:
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁶ : CommSemiring R✝
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
inst✝² : Semiring B
inst✝¹ : Algebra R✝ B
R : Type ?u.22
A : Type ?u.24
x✝¹ : CommSemiring R
x✝ : Semiring A
inst✝ : Algebra R A
⊢ ∀ (a : R), a • 0 = 0

Tactic:
by simp [smul_def']

Goal state after:
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁶ : CommSemiring R✝
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
inst✝² : Semiring B
inst✝¹ : Algebra R✝ B
R : Type ?u.22
A : Type ?u.24
x✝¹ : CommSemiring R
x✝ : Semiring A
inst✝ : Algebra R A
⊢ ∀ (x : A), 0 • x = 0

Tactic:
by simp [smul_def']

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MulZeroClass (α i)
inst✝ : DecidableEq ι
i : ι
f : (i : ι) → α i
⊢ ∀ (a : (i : ι) → α i), 0 * a = 0

Tactic:
intros

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MulZeroClass (α i)
inst✝ : DecidableEq ι
i : ι
f a✝ : (i : ι) → α i
⊢ 0 * a✝ = 0
Module: Mathlib.Algebra.GroupWithZero.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MulZeroClass (α i)
inst✝ : DecidableEq ι
i : ι
f : (i : ι) → α i
⊢ ∀ (a : (i : ι) → α i), a * 0 = 0

Tactic:
intros

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MulZeroClass (α i)
inst✝ : DecidableEq ι
i : ι
f a✝ : (i : ι) → α i
⊢ a✝ * 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Action.Pi

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → Zero (g i)
inst✝ : (i : I) → SMulZeroClass (f i) (g i)
⊢ ∀ (a : (i : I) → f i), a • 0 = 0

Tactic:
intros

Goal state after:
I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → Zero (g i)
inst✝ : (i : I) → SMulZeroClass (f i) (g i)
a✝ : (i : I) → f i
⊢ a✝ • 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Action.Pi

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst✝ : (i : I) → DistribSMul (f i) (g i)
⊢ ∀ (a : (i : I) → f i), a • 0 = 0

Tactic:
intros

Goal state after:
I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst✝ : (i : I) → DistribSMul (f i) (g i)
a✝ : (i : I) → f i
⊢ a✝ • 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Action.Pi

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst✝ : (i : I) → DistribSMul (f i) (g i)
⊢ ∀ (a : (i : I) → f i) (x y : (i : I) → g i), a • (x + y) = a • x + a • y

Tactic:
intros

Goal state after:
I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst✝ : (i : I) → DistribSMul (f i) (g i)
a✝ : (i : I) → f i
x✝ y✝ : (i : I) → g i
⊢ a✝ • (x✝ + y✝) = a✝ • x✝ + a✝ • y✝
Module: Mathlib.Algebra.GroupWithZero.Action.Pi

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst✝ : (i : I) → MulDistribMulAction (f i) (g i)
⊢ ∀ (r : (i : I) → f i), r • 1 = 1

Tactic:
intros

Goal state after:
I : Type u
f : I → Type v
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst✝ : (i : I) → MulDistribMulAction (f i) (g i)
r✝ : (i : I) → f i
⊢ r✝ • 1 = 1
Module: Mathlib.Algebra.GroupWithZero.Action.Pi

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst✝ : (i : I) → MulDistribMulAction (f i) (g i)
⊢ ∀ (r : (i : I) → f i) (x y : (i : I) → g i), r • (x * y) = r • x * r • y

Tactic:
intros

Goal state after:
I : Type u
f : I → Type v
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst✝ : (i : I) → MulDistribMulAction (f i) (g i)
r✝ : (i : I) → f i
x✝ y✝ : (i : I) → g i
⊢ r✝ • (x✝ * y✝) = r✝ • x✝ * r✝ • y✝
Module: Mathlib.Algebra.Module.Pi

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
⊢ ∀ (r_1 s : (i : I) → f i) (x : (i : I) → g i), (r_1 + s) • x = r_1 • x + s • x

Tactic:
intros

Goal state after:
I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
r✝ s✝ : (i : I) → f i
x✝ : (i : I) → g i
⊢ (r✝ + s✝) • x✝ = r✝ • x✝ + s✝ • x✝
Module: Mathlib.Algebra.Module.Pi

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
⊢ ∀ (x : (i : I) → g i), 0 • x = 0

Tactic:
intros

Goal state after:
I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
x✝ : (i : I) → g i
⊢ 0 • x✝ = 0
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
⊢ ∀ (x y : M →ₛₗ[σ₁₂] M₂), (x + y).toAddMonoidHom = x.toAddMonoidHom + y.toAddMonoidHom

Tactic:
intros

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
x✝ y✝ : M →ₛₗ[σ₁₂] M₂
⊢ (x✝ + y✝).toAddMonoidHom = x✝.toAddMonoidHom + y✝.toAddMonoidHom
Module: Mathlib.Algebra.Ring.Pi

Goal state before:
pp: I : Type u
f : I → Type v
i : I
inst✝ : (i : I) → Distrib (f i)
⊢ ∀ (a b c : (i : I) → f i), a * (b + c) = a * b + a * c

Tactic:
intros

Goal state after:
I : Type u
f : I → Type v
i : I
inst✝ : (i : I) → Distrib (f i)
a✝ b✝ c✝ : (i : I) → f i
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝
Module: Mathlib.Algebra.Ring.Pi

Goal state before:
pp: I : Type u
f : I → Type v
i : I
inst✝ : (i : I) → Distrib (f i)
⊢ ∀ (a b c : (i : I) → f i), (a + b) * c = a * c + b * c

Tactic:
intros

Goal state after:
I : Type u
f : I → Type v
i : I
inst✝ : (i : I) → Distrib (f i)
a✝ b✝ c✝ : (i : I) → f i
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝
Module: Mathlib.Algebra.Ring.PUnit

Goal state before:
pp: ⊢ ∀ (a : PUnit), 0 * a = 0

Tactic:
intros

Goal state after:
a✝ : PUnit
⊢ 0 * a✝ = 0
Module: Mathlib.Algebra.Ring.PUnit

Goal state before:
pp: ⊢ ∀ (a : PUnit), a * 0 = 0

Tactic:
intros

Goal state after:
a✝ : PUnit
⊢ a✝ * 0 = 0
Module: Mathlib.Algebra.Ring.PUnit

Goal state before:
pp: ⊢ ∀ (a b c : PUnit), a * (b + c) = a * b + a * c

Tactic:
intros

Goal state after:
a✝ b✝ c✝ : PUnit
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝
Module: Mathlib.Algebra.Ring.PUnit

Goal state before:
pp: ⊢ ∀ (a b c : PUnit), (a + b) * c = a * c + b * c

Tactic:
intros

Goal state after:
a✝ b✝ c✝ : PUnit
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S✝ M
inst✝¹ : SMul S✝ R
inst✝ : IsScalarTower S✝ R M
p q : Submodule R M
S : Set (Submodule R M)
⊢ 0 ∈ ⋂ s ∈ S, ↑s

Tactic:
by simp [zero_mem]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q✝ p q : Submodule R M
⊢ 0 ∈ ↑p ∩ ↑q

Tactic:
by simp [zero_mem]

Goal state after:
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst✝² : CommSemiring R
inst✝¹ : (x : M) → AddCommMonoid (V x)
inst✝ : (x : M) → Module R (V x)
e : (x : M) → V x →ₗ[R] R
⊢ ∀ (x y : (x : M) → V x), (fun x_1 ↦ (e x_1) ((x + y) x_1)) = (fun x_1 ↦ (e x_1) (x x_1)) + fun x ↦ (e x) (y x)

Tactic:
intros

Goal state after:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst✝² : CommSemiring R
inst✝¹ : (x : M) → AddCommMonoid (V x)
inst✝ : (x : M) → Module R (V x)
e : (x : M) → V x →ₗ[R] R
x✝ y✝ : (x : M) → V x
⊢ (fun x ↦ (e x) ((x✝ + y✝) x)) = (fun x ↦ (e x) (x✝ x)) + fun x ↦ (e x) (y✝ x)
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst✝² : CommSemiring R
inst✝¹ : (x : M) → AddCommMonoid (V x)
inst✝ : (x : M) → Module R (V x)
e : (x : M) → V x →ₗ[R] R
⊢ ∀ (m : R) (x : (x : M) → V x), (fun x_1 ↦ (e x_1) ((m • x) x_1)) = (RingHom.id R) m • fun x_1 ↦ (e x_1) (x x_1)

Tactic:
intros

Goal state after:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst✝² : CommSemiring R
inst✝¹ : (x : M) → AddCommMonoid (V x)
inst✝ : (x : M) → Module R (V x)
e : (x : M) → V x →ₗ[R] R
m✝ : R
x✝ : (x : M) → V x
⊢ (fun x ↦ (e x) ((m✝ • x✝) x)) = (RingHom.id R) m✝ • fun x ↦ (e x) (x✝ x)
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst✝² : CommSemiring R
inst✝¹ : (x : M) → AddCommMonoid (V x)
inst✝ : (x : M) → Module R (V x)
⊢ ∀ (x y : (x : M) → V x →ₗ[R] R),
    { toFun := fun s x_1 ↦ ((x + y) x_1) (s x_1), map_add' := ⋯, map_smul' := ⋯ } =
      { toFun := fun s x_1 ↦ (x x_1) (s x_1), map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun s x ↦ (y x) (s x), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
intros

Goal state after:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst✝² : CommSemiring R
inst✝¹ : (x : M) → AddCommMonoid (V x)
inst✝ : (x : M) → Module R (V x)
x✝ y✝ : (x : M) → V x →ₗ[R] R
⊢ { toFun := fun s x ↦ ((x✝ + y✝) x) (s x), map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun s x ↦ (x✝ x) (s x), map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun s x ↦ (y✝ x) (s x), map_add' := ⋯, map_smul' := ⋯ }
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst✝² : CommSemiring R
inst✝¹ : (x : M) → AddCommMonoid (V x)
inst✝ : (x : M) → Module R (V x)
⊢ ∀ (m : R) (x : (x : M) → V x →ₗ[R] R),
    { toFun := fun s x_1 ↦ ((m • x) x_1) (s x_1), map_add' := ⋯, map_smul' := ⋯ } =
      (RingHom.id R) m • { toFun := fun s x_1 ↦ (x x_1) (s x_1), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
intros

Goal state after:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst✝² : CommSemiring R
inst✝¹ : (x : M) → AddCommMonoid (V x)
inst✝ : (x : M) → Module R (V x)
m✝ : R
x✝ : (x : M) → V x →ₗ[R] R
⊢ { toFun := fun s x ↦ ((m✝ • x✝) x) (s x), map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) m✝ • { toFun := fun s x ↦ (x✝ x) (s x), map_add' := ⋯, map_smul' := ⋯ }
Module: Mathlib.Algebra.Module.Submodule.LinearMap

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
p : Submodule R M
n : ℕ
h : ∀ x ∈ p, f' x ∈ p
x : M
hx : x ∈ p
⊢ (f' ^ n) x ∈ p

Tactic:
induction n generalizing x with

Goal state after:
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝¹ : FunLike F α β
inst✝ : SupSet α
x✝ : CompleteLattice β
s : Set α
⊢ ⊥ = sSup ((fun x ↦ ⊥) '' s)

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Goal state after:
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝¹ : FunLike F α β
inst✝ : SupSet α
x✝ : CompleteLattice β
⊢ ⊥ = sSup ((fun x ↦ ⊥) '' ∅)

case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝¹ : FunLike F α β
inst✝ : SupSet α
x✝ : CompleteLattice β
s : Set α
hs : s.Nonempty
⊢ ⊥ = sSup ((fun x ↦ ⊥) '' s)