mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u}
α : Type u
s : Set α
⊢ ∀ (a : Set ↑s), #↑a = c ↔ #↑(Subtype.val '' a) = c

Tactic:
intro t

Goal state after:
c : Cardinal.{u}
α : Type u
s : Set α
t : Set ↑s
⊢ #↑t = c ↔ #↑(Subtype.val '' t) = c
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
r : R
y : A
⊢ x * (algebraMap R A) r * y = x * y * (algebraMap R A) r

Tactic:
rw [mul_assoc, commutes, ← mul_assoc]

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

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst✝³ : Semiring S
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module S M
s s' : Sᵈᵐᵃ
f : M →+ M₂
m : M
⊢ f (DomMulAct.mk.symm (s + s') • m) = f (DomMulAct.mk.symm s • m) + f (DomMulAct.mk.symm s' • m)

Tactic:
← map_add,

Goal state after:
R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst✝³ : Semiring S
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module S M
s s' : Sᵈᵐᵃ
f : M →+ M₂
m : M
⊢ f (DomMulAct.mk.symm (s + s') • m) = f (DomMulAct.mk.symm s • m + DomMulAct.mk.symm s' • m)
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:
by intros; ext x; exact smul_zero _

Goal state after:
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:
by intros; ext x; exact smul_zero _

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r : R
m : M
inst✝¹ : IsTorsionFree R M
inst✝ : IsCancelMulZero R
⊢ r • m = 0 ↔ r = 0 ∨ m = 0

Tactic:
obtain rfl | hr := eq_or_ne r 0 <;> simp [smul_eq_zero_iff_right, *]

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R'
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R' M'
σ₁₂ : R →+* R'
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module S M'
inst✝¹ : SMulCommClass R' S M'
inst✝ : SMulCommClass R S M
x✝³ x✝² : Sᵈᵐᵃ
x✝¹ : M →ₛₗ[σ₁₂] M'
x✝ : M
⊢ x✝¹ (DomMulAct.mk.symm (x✝³ + x✝²) • x✝) = x✝¹ (DomMulAct.mk.symm x✝³ • x✝) + x✝¹ (DomMulAct.mk.symm x✝² • x✝)

Tactic:
← map_add,

Goal state after:
R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R'
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R' M'
σ₁₂ : R →+* R'
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module S M'
inst✝¹ : SMulCommClass R' S M'
inst✝ : SMulCommClass R S M
x✝³ x✝² : Sᵈᵐᵃ
x✝¹ : M →ₛₗ[σ₁₂] M'
x✝ : M
⊢ x✝¹ (DomMulAct.mk.symm (x✝³ + x✝²) • x✝) = x✝¹ (DomMulAct.mk.symm x✝³ • x✝ + DomMulAct.mk.symm x✝² • x✝)
Module: Mathlib.Algebra.Module.Submodule.LinearMap

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
inst✝¹³ : Semiring R
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
M₂' : Type u_10
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective ⇑p
h : ∀ (c : M), f c ∈ range ⇑p
b c : M
⊢ p ⋯.choose = f b + f c

Tactic:
← map_add,

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
inst✝¹³ : Semiring R
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
M₂' : Type u_10
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective ⇑p
h : ∀ (c : M), f c ∈ range ⇑p
b c : M
⊢ p ⋯.choose = f (b + c)
Module: Mathlib.Algebra.Module.Submodule.LinearMap

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
inst✝¹³ : Semiring R
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
M₂' : Type u_10
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective ⇑p
h : ∀ (c : M), f c ∈ range ⇑p
b c : M
⊢ p (Exists.choose ⋯) = p (Exists.choose ⋯ + Exists.choose ⋯)

Tactic:
simp_rw [map_add, (h _).choose_spec, ← map_add, (h _).choose_spec]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⊥ = ⊤ ↔ ⊥ = ⊤

Tactic:
← toAddSubmonoid_inj,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⊥.toAddSubmonoid = ⊤.toAddSubmonoid ↔ ⊥ = ⊤
Module: Mathlib.Algebra.Module.ULift

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝² : Monoid R
inst✝¹ : Monoid M
inst✝ : MulDistribMulAction R M
x✝ : R
⊢ x✝ • 1 = 1

Tactic:
ext
      simp [smul_one]

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
⊢ Disjoint p q ↔ comap p.subtype q = ⊥

Tactic:
by
  rw [← (map_injective_of_injective (show Injective p.subtype from Subtype.coe_injective)).eq_iff,
    map_comap_subtype, map_bot, disjoint_iff]

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
sg : Subsemigroup R
sa : AddSubmonoid R
ha : ↑sa = ↑sg
⊢ ∀ {a b : R}, a ∈ ↑sg → b ∈ ↑sg → a * b ∈ ↑sg

Tactic:
exact sg.mul_mem

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
p : Prop
S : p → Subsemigroup M
x : M
⊢ x ∈ ⨆ (h : p), S h ↔ ∃ (h : p), x ∈ S h

Tactic:
by
  by_cases h : p
  · simp +contextual [h]
  · simpa [h] using! id

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
S : Set (Subsemigroup M)
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ s ∈ S, ↑s

Tactic:
by simp [mem_sSup_of_directed_on hS]

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure.toNonUnitalSubsemiring
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M

Tactic:
· simp only [Subsemiring.mem_toNonUnitalSubsemiring, subsemiringClosure_mem] at hx
    induction hx using AddSubmonoid.closure_induction <;> aesop

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝² : A →ₐ[R] A
x✝¹ x✝ : Aˣ
⊢ x✝² • (x✝¹ * x✝) = x✝² • x✝¹ * x✝² • x✝

Tactic:
ext; exact map_mul _ _ _

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : x ∈ closure s), p x 1 hx ⋯
neg_left : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p (-x) y ⋯ hy
neg_right : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : x ∈ closure s
hy : y ∈ closure s
⊢ p x y hx hy

Tactic:
by
  induction hy using closure_induction with
  | mem z hz => induction hx using closure_induction with
    | mem _ h => exact mem_mem _ _ h hz
    | zero => exact zero_left _ _
    | one => exact one_left _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
    | neg _ _ h => exact neg_left _ _ _ _ h
  | zero => exact zero_right x hx
  | one => exact one_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
  | neg _ _ h => exact neg_right _ _ _ _ h

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
n : ℕ
x✝ : Prime p ∧ n = 1
hp : Prime p
hn : n = 1
⊢ Prime (p ^ n)

Tactic:
by simpa [hn]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p q : M
h : DvdNotUnit p q
⊢ ¬p ~ᵤ q

Tactic:
by
  rintro ⟨a, rfl⟩
  obtain ⟨hp, x, hx, hx'⟩ := h
  rcases (mul_right_inj' hp).mp hx' with rfl
  exact hx a.isUnit

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective ⇑i
hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range
e : ↥i.range ≃ₗ[R] M₃ := (LinearEquiv.ofInjective i hi).symm
⊢ ∀ (m : R) (x : M₁), ↑e ∘ₗ codRestrict i.range (f (m • x)) ⋯ = (RingHom.id R) m • ↑e ∘ₗ codRestrict i.range (f x) ⋯

Tactic:
intro t

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective ⇑i
hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range
e : ↥i.range ≃ₗ[R] M₃ := (LinearEquiv.ofInjective i hi).symm
t : R
⊢ ∀ (x : M₁), ↑e ∘ₗ codRestrict i.range (f (t • x)) ⋯ = (RingHom.id R) t • ↑e ∘ₗ codRestrict i.range (f x) ⋯
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ y z, ↑y + ↑z = x

Tactic:
simp only [Subtype.exists, exists_prop]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
⊢ (image g s).SupIndep f

Tactic:
intro t

Goal state after:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι
⊢ t ⊆ image g s → ∀ ⦃i : ι⦄, i ∈ image g s → i ∉ t → Disjoint (f i) (t.sup f)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_2.inr
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
hjk : j ≠ k
⊢ v k ∈ span R (range (update v j (v j + r • v i)))

Tactic:
exact subset_span ⟨k, update_of_ne hjk.symm ..⟩

Goal state after:
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a : α
⊢ ⇑e '' Iio a = Iio (e a)

Tactic:
rw [e.image_eq_preimage_symm, e.symm.preimage_Iio, e.symm_symm]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_2
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ s i ∈ lowerBounds (upperBounds (Function.eval i '' {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s}))

Tactic:
refine fun j hj ↦ (isLUB_atoms_le (s i)).2 fun x ⟨hx₁, hx₂⟩ ↦ ?_

Goal state after:
case refine_2
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
j : π i
hj : j ∈ upperBounds (Function.eval i '' {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s})
x : π i
x✝ : x ∈ {a | IsAtom a ∧ a ≤ s i}
hx₁ : IsAtom x
hx₂ : x ≤ s i
⊢ x ≤ j
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case h
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := ⋯
dir_US : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : α
hx : x ∈ s
⊢ ↑{x} ⊆ s ∧ x = {x}.sup id

Tactic:
simpa only [and_true, id, Finset.coe_singleton, eq_self_iff_true,
          Finset.sup_singleton, Set.singleton_subset_iff]

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

Goal state before:
pp: case refine_2
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝¹ : A
hp : x✝¹ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
x✝ y✝ : S
hx✝ : x✝ ∈ span R s
hy✝ : y✝ ∈ span R s
⊢ x✝ • y ∈ span R (s • t) → y✝ • y ∈ span R (s • t) → x✝ • y + y✝ • y ∈ span R (s • t)

Tactic:
apply add_mem

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

Goal state before:
pp: case refine_2
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
⊢ ∀ (x y_1 : S),
    x ∈ span R s → y_1 ∈ span R s → x • y ∈ span R (s • t) → y_1 • y ∈ span R (s • t) → (x + y_1) • y ∈ span R (s • t)

Tactic:
intro _ _ _ _; rw [add_smul]; apply add_mem

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
S : Set M
f g : ↥(span R S) →ₗ[R] N
h : ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
x : M
hx : x ∈ span R S
⊢ f ⟨x, hx⟩ = g ⟨x, hx⟩

Tactic:
induction hx using span_induction with
    | mem x hx => exact h ⟨x, hx⟩
    | zero => erw [map_zero, map_zero]
    | add x y hx hy hx' hy' =>
        erw [f.map_add ⟨x, hx⟩ ⟨y, hy⟩, g.map_add ⟨x, hx⟩ ⟨y, hy⟩]
        rw [hx', hy']
    | smul a x hx hx' =>
        erw [f.map_smul a ⟨x, hx⟩, g.map_smul a ⟨x, hx⟩]
        rw [hx']

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → sSupIndep ↑t
a : α
ha : a ∈ s
⊢ ∀ (i : Finset α), ⨆ (_ : ↑i ⊆ s \ {a}), a ⊓ i.sup id = ⊥

Tactic:
intro t

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → sSupIndep ↑t
a : α
ha : a ∈ s
t : Finset α
⊢ ⨆ (_ : ↑t ⊆ s \ {a}), a ⊓ t.sup id = ⊥
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
⊢ span S (range ⇑(inclusionSpan S p)) = ⊤

Tactic:
have : (span S (p : Set M)).subtype '' range (inclusionSpan S p) = p := by
    ext; simpa [Subtype.ext_iff] using! fun h ↦ subset_span h

Goal state after:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
this : ⇑(span S ↑p).subtype '' range ⇑(inclusionSpan S p) = ↑p
⊢ span S (range ⇑(inclusionSpan S p)) = ⊤
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
⊢ ∀ (t : Finset α), ↑t ⊆ ⋃ i, s i → sSupIndep ↑t

Tactic:
intro t

Goal state after:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
t : Finset α
⊢ ↑t ⊆ ⋃ i, s i → sSupIndep ↑t
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case refine_4.refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
x✝¹ : M
hx✝ : x✝¹ ∈ span R (⋃ i, ↑(p i))
r : R
x : M
x✝ : x ∈ span R (⋃ i, ↑(p i))
hx : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ ∀ (x y : M),
    x ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) →
      y ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) →
        r • x ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) →
          r • y ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) → r • (x + y) ∈ AddSubmonoid.closure (⋃ i, ↑(p i))

Tactic:
· intro x y _ _ hx hy
      rw [smul_add]
      exact AddSubmonoid.add_mem _ hx hy

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: M₀ : Type u_4
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
a : M₀
l : List M₀
⊢ (a :: l).prod = 0 ↔ 0 ∈ a :: l

Tactic:
rw [prod_cons, mul_eq_zero, prod_eq_zero_iff, mem_cons, eq_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y : N
hx : x ∈ span R s
hy : y ∈ span R t
⊢ (B x) y ∈ P'

Tactic:
by
  induction hx, hy using span_induction₂ with
  | mem_mem u v hu hv => exact hB u hu v hv
  | zero_left v hv => simp
  | zero_right u hu => simp
  | add_left u₁ u₂ v hu₁ hu₂ hv huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | add_right u v₁ v₂ hu hv₁ hv₂ huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | smul_left t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
  | smul_right t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
⊢ ⟨x, hx⟩ ∈ ⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i)

Tactic:
suffices x ∈ (⨆ i ∈ s, (p i).comap (⨆ i ∈ s, p i).subtype).map (⨆ i ∈ s, (p i)).subtype by
    obtain ⟨y, hy, rfl⟩ := Submodule.mem_map.mp this
    exact hy

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
⊢ x ∈ map (⨆ i ∈ s, p i).subtype (⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i))
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
m n : ℕ
f g : ℕ → R
⊢ (∑ i ∈ range (m + 1), f i) * ∑ i ∈ range (n + 1), g i =
    (∑ i ∈ range m, f i) * ∑ i ∈ range n, g i + f m * ∑ i ∈ range n, g i + (∑ i ∈ range m, f i) * g n + f m * g n

Tactic:
by
  simp only [add_mul, mul_add, add_assoc, sum_range_succ]

Goal state after:
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: ι : Type u_6
inst✝¹ : DecidableEq ι
M : Type u_7
inst✝ : One M
i : ι
f : ι → M
j : ι
⊢ {i}.mulIndicator f j = Pi.mulSingle i (f i) j

Tactic:
simp only [Set.mulIndicator_apply, Pi.mulSingle_apply, Set.mem_singleton_iff]

Goal state after:
ι : Type u_6
inst✝¹ : DecidableEq ι
M : Type u_7
inst✝ : One M
i : ι
f : ι → M
j : ι
⊢ (if j = i then f j else 1) = if j = i then f i else 1
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝¹ : Zero M
inst✝ : IsEmpty α
f g : α →₀ M
x : α
⊢ f x = g x

Tactic:
exact isEmptyElim x

Goal state after:
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
⊢ motive f

Tactic:
have hs' : (erase a f).support = s := by
      rw [support_erase, hs, erase_insert (fun ha => (hm a ha).false)]

Goal state after:
case refine_2
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
hs' : (erase a f).support = s
⊢ motive f
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : Zero M
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f1 f2 : α →₀ M
g1 g2 : α → M → N
h : ∀ x ∈ f1.support ∪ f2.support, g1 x (f1 x) = g2 x (f2 x)
h1 : ∀ x ∈ f1.support ∪ f2.support, g1 x 0 = 1
h2 : ∀ x ∈ f1.support ∪ f2.support, g2 x 0 = 1
⊢ f1.prod g1 = f2.prod g2

Tactic:
rw [Finsupp.prod_of_support_subset f1 Finset.subset_union_left _ h1,
    Finsupp.prod_of_support_subset f2 Finset.subset_union_right _ h2]

Goal state after:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : Zero M
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f1 f2 : α →₀ M
g1 g2 : α → M → N
h : ∀ x ∈ f1.support ∪ f2.support, g1 x (f1 x) = g2 x (f2 x)
h1 : ∀ x ∈ f1.support ∪ f2.support, g1 x 0 = 1
h2 : ∀ x ∈ f1.support ∪ f2.support, g2 x 0 = 1
⊢ ∏ x ∈ f1.support ∪ f2.support, g1 x (f1 x) = ∏ x ∈ f1.support ∪ f2.support, g2 x (f2 x)