mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ compHom α (MonoidHom.inl M N) = hM

pp: case e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ ⟨compHom α (MonoidHom.inr M N), ⋯⟩ ≍ ⟨hN, snd✝⟩

Tactic:
· ext m a; (conv_rhs => rw [← hN.one_smul a]); rfl

Goal state after:
case e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ ⟨compHom α (MonoidHom.inr M N), ⋯⟩ ≍ ⟨hN, snd✝⟩
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 S✝
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M₃
inst✝¹⁰ : Module R✝ M
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module S✝ M₃
σ : R✝ →+* S✝
fₗ✝ : M →ₗ[R✝] M₂
f g : M →ₛₗ[σ] M₃
R : Type u_14
S : Type u_15
inst✝⁷ : Semiring S
inst✝⁶ : SMul R M
inst✝⁵ : Module S M
inst✝⁴ : SMul R M₂
inst✝³ : Module S M₂
inst✝² : SMul R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S M₂
fₗ : M →ₗ[S] M₂
c : R
x : M
⊢ fₗ ((c • 1) • x) = c • fₗ x

Tactic:
← smul_one_smul S c (fₗ x),

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 S✝
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M₃
inst✝¹⁰ : Module R✝ M
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module S✝ M₃
σ : R✝ →+* S✝
fₗ✝ : M →ₗ[R✝] M₂
f g : M →ₛₗ[σ] M₃
R : Type u_14
S : Type u_15
inst✝⁷ : Semiring S
inst✝⁶ : SMul R M
inst✝⁵ : Module S M
inst✝⁴ : SMul R M₂
inst✝³ : Module S M₂
inst✝² : SMul R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S M₂
fₗ : M →ₗ[S] M₂
c : R
x : M
⊢ fₗ ((c • 1) • x) = (c • 1) • fₗ x
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:
by intros; ext x; exact smul_add _ _ _

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

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 S M
σ : Rᵐᵒᵖ →+* S
f g : R →ₛₗ[σ] M
h : f 1 = g 1
x : R
⊢ σ (MulOpposite.op x) • g 1 = g (MulOpposite.op x • 1)

Tactic:
g.map_smulₛₗ

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
σ : Rᵐᵒᵖ →+* S
f g : R →ₛₗ[σ] M
h : f 1 = g 1
x : R
⊢ σ (MulOpposite.op x) • g 1 = σ (MulOpposite.op x) • g 1
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R' : Type u_4
M' : Type u_5
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
S T : Submodule R' M'
s t : M'
hs : s ∈ S
ht : t ∈ T
⊢ s - t ∈ S ⊔ T

Tactic:
sub_eq_add_neg

Goal state after:
R' : Type u_4
M' : Type u_5
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
S T : Submodule R' M'
s t : M'
hs : s ∈ S
ht : t ∈ T
⊢ s + -t ∈ S ⊔ T
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
s : Set (Submodule R M)
t : R
m : M
h : m ∈ sSup (toAddSubmonoid '' s)
⊢ t • m ∈ sSup (toAddSubmonoid '' s)

Tactic:
sSup_eq_iSup'

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
⊢ t • m ∈ ⨆ a, ↑a
Module: Mathlib.Algebra.Module.Submodule.RestrictScalars

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
s : Set (Submodule R M)
⊢ restrictScalars S (sSup s) = sSup (restrictScalars S '' s)

Tactic:
by
  simp [← toAddSubmonoid_inj, toAddSubmonoid_sSup, ← Set.image_comp]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
s : Set R
sm : Submonoid R
hm : ↑sm = s
sa : AddSubmonoid R
ha : ↑sa = s
x y : R
⊢ x ∈ s → y ∈ s → x + y ∈ s

Tactic:
simpa only [← ha] using! sa.add_mem

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonAssocRing R
s : Subsemiring R
hneg : -1 ∈ s
x✝ : R
h : x✝ ∈ s.carrier
⊢ -x✝ ∈ s.carrier

Tactic:
rw [← neg_one_mul]
    exact mul_mem hneg h

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
S : Subring R
⊢ S.toNonUnitalSubring.toSubring ⋯ = S

Tactic:
cases S

Goal state after:
case mk
R : Type u
inst✝ : NonAssocRing R
toSubsemiring✝ : Subsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toSubsemiring✝.carrier → -x ∈ toSubsemiring✝.carrier
⊢ { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }.toNonUnitalSubring.toSubring ⋯ =
    { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }
Module: Mathlib.Algebra.Ring.Subring.Defs

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
S : NonUnitalSubring R
h1 : 1 ∈ S
⊢ (S.toSubring h1).toNonUnitalSubring = S

Tactic:
cases S

Goal state after:
case mk
R : Type u
inst✝ : NonAssocRing R
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }.toSubring h1).toNonUnitalSubring =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝¹ x✝ : M
⊢ x✝¹ * (x✝ * a) + x✝¹ * x✝ * b = x✝¹ * (x✝ * (a + b))

Tactic:
hb.right_assoc,

Goal state after:
M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝¹ x✝ : M
⊢ x✝¹ * (x✝ * a) + x✝¹ * (x✝ * b) = x✝¹ * (x✝ * (a + b))
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup M
⊢ ∀ {a b : N}, a ∈ ⇑f '' ↑S → b ∈ ⇑f '' ↑S → a * b ∈ ⇑f '' ↑S

Tactic:
rintro _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup M
x : M
hx : x ∈ ↑S
y : M
hy : y ∈ ↑S
⊢ f x * f y ∈ ⇑f '' ↑S
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
s : Set R
x x✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hL : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x✝
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = -x✝

Tactic:
obtain ⟨L, hL⟩ := hL

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
s : Set R
x x✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
L : List (List R)
hL : (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x✝
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = -x✝
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case refine_2
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : ↑u * y = A * B
⊢ IsUnit A ∨ IsUnit B

Tactic:
rw [← u⁻¹.isUnit_units_mul]

Goal state after:
case refine_2
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : ↑u * y = A * B
⊢ IsUnit (↑u⁻¹ * A) ∨ IsUnit B
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
⊢ C hd.prod

Tactic:
clear ih tl

Goal state after:
case cons
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
⊢ C hd.prod
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons.inr.cons
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ x ∈ tl, x ∈ s) → C (-tl.prod)
HL' : ∀ x ∈ hd :: tl, x ∈ s
⊢ C (-(hd * tl.prod))

Tactic:
neg_mul_eq_mul_neg

Goal state after:
case cons.inr.cons
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ x ∈ tl, x ∈ s) → C (-tl.prod)
HL' : ∀ x ∈ hd :: tl, x ∈ s
⊢ C (hd * -tl.prod)
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = L.prod
hhd : hd = -1
⊢ (hd :: tl).prod = -L.prod

Tactic:
by rw [List.prod_cons, hhd, neg_one_mul, HP]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = -L.prod
hhd : hd ∈ s
⊢ hd * -L.prod = -(hd * L.prod)

Tactic:
neg_mul_eq_mul_neg

Goal state after:
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = -L.prod
hhd : hd ∈ s
⊢ hd * -L.prod = hd * -L.prod
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case mp.mk.refine_1
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ x * a = 0

Tactic:
rwa [← Associates.mk_eq_zero, ← Associates.mk_mul_mk, ← Associates.quot_mk_eq_mk]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q r : M
h : DvdNotUnit p q
h' : q ~ᵤ r
⊢ DvdNotUnit p r

Tactic:
by
  obtain ⟨u, rfl⟩ := h'
  obtain ⟨hp, x, hx⟩ := h
  refine ⟨hp, x * u, mt isUnit_of_mul_isUnit_left hx.1, ?_⟩
  rw [← mul_assoc, ← hx.right]

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 x; ext y; simp [f.map_smul, ← e.map_smul, codRestrict]

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ c (x ⊔ c y) = c (x ⊔ y)

Tactic:
rw [sup_comm, closure_sup_closure_left, sup_comm (a := x)]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a : α
⊢ Iio a = {⊥} ↔ IsAtom a

Tactic:
simp [IsAtom, superset_antisymm_iff, bot_lt_iff_ne_bot]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
b : α
a : ↑(Iic b)
⊢ a ⋖ ⊤ ↔ ↑a ⋖ b

Tactic:
refine (Set.OrdConnected.apply_covBy_apply_iff (OrderEmbedding.subtype fun c => c ≤ b) ?_).symm

Goal state after:
α : Type u_2
inst✝ : PartialOrder α
b : α
a : ↑(Iic b)
⊢ (range ⇑(OrderEmbedding.subtype fun c ↦ c ≤ b)).OrdConnected
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
s : Submodule R M
v₀ : M
⊢ (∀ ⦃x : M⦄, x ∈ s → x ∈ R ∙ v₀) ↔ ∀ v ∈ s, ∃ r, r • v₀ = v

Tactic:
mem_span_singleton

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x : M
hx : x ∈ span R S
⊢ ∃ T, ↑T ⊆ S ∧ 0 ∈ span R ↑T

pp: case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x : M
hx : x ∈ span R S
⊢ ∀ (x y : M),
    x ∈ span R S →
      y ∈ span R S → (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → (∃ T, ↑T ⊆ S ∧ y ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ x + y ∈ span R ↑T

pp: case refine_4
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x : M
hx : x ∈ span R S
⊢ ∀ (a : R), ∀ x ∈ span R S, (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ a • x ∈ span R ↑T

Tactic:
· use ∅
    simp

Goal state after:
case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x : M
hx : x ∈ span R S
⊢ ∀ (x y : M),
    x ∈ span R S →
      y ∈ span R S → (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → (∃ T, ↑T ⊆ S ∧ y ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ x + y ∈ span R ↑T

case refine_4
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x : M
hx : x ∈ span R S
⊢ ∀ (a : R), ∀ x ∈ span R S, (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ a • x ∈ span R ↑T
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
s : Set M
t : Finset M
ht : ↑t ⊆ ↑(span R s)
⊢ ∃ T, ↑T ⊆ s ∧ ↑t ⊆ ↑(span R ↑T)

Tactic:
by
  classical
  induction t using Finset.induction_on with
  | empty => exact ⟨∅, by simp⟩
  | insert a t hat IH =>
    obtain ⟨T, hTs, htT⟩ := IH (by simp_all [Set.insert_subset_iff])
    obtain ⟨T', hT's, haT'⟩ := mem_span_finite_of_mem_span (ht (Finset.mem_insert_self _ _))
    refine ⟨T ∪ T', by simp_all, ?_⟩
    simp only [Finset.coe_insert, Finset.coe_union, span_union, insert_subset_iff, SetLike.mem_coe]
    exact ⟨mem_sup_right haT', htT.trans (le_sup_left (a := span R _))⟩

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this✝ : Finite ↑t
this : Nonempty ↑t
⊢ sSup t ∈ s

Tactic:
sSup_eq_iSup'

Goal state after:
α : Type u_3
inst✝ : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this✝ : Finite ↑t
this : Nonempty ↑t
⊢ ⨆ a, ↑a ∈ s
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hts : t ⊆ s
this : Finite ↑t
⊢ sSup t ∈ s

Tactic:
sSup_eq_iSup'

Goal state after:
α : Type u_3
inst✝ : CompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hts : t ⊆ s
this : Finite ↑t
⊢ ⨆ a, ↑a ∈ s
Module: Mathlib.Order.Interval.Set.OrderIso

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

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

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : (map g s).SupIndep f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit : i ∉ t
⊢ Disjoint ((f ∘ ⇑g) i) (t.sup (f ∘ ⇑g))

Tactic:
rw [← sup_map]

Goal state after:
case refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : (map g s).SupIndep f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit : i ∉ t
⊢ Disjoint ((f ∘ ⇑g) i) ((map g t).sup f)
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomic (π i)
b : (i : ι) → π i
h : ¬b = ⊥
i : ι
hi : ¬b i = ⊥
a : π i
ha : IsAtom a
hab : a ≤ b i
⊢ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
by classical exact ⟨Function.update ⊥ i a, isAtom_single ha, update_le_iff.2 ⟨hab, by simp⟩⟩

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
⊢ iSupIndep t ↔ Disjoint (t i) (t j)

Tactic:
constructor
  · exact fun h => h.pairwiseDisjoint hij
  · rintro h k
    obtain rfl | rfl := huniv k
    · refine h.mono_right (iSup_le fun i => iSup_le fun hi => Eq.le ?_)
      rw [(huniv i).resolve_left hi]
    · refine h.symm.mono_right (iSup_le fun j => iSup_le fun hj => Eq.le ?_)
      rw [(huniv j).resolve_right hj]

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
⊢ s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x

Tactic:
hne

Goal state after:
case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
hne : s.Nonempty
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1
⊢ ∀ (s_1 : Set α), s_1.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s_1 → s.sup f ≤ sSup s_1 → ∃ x ∈ s_1, s.sup f ≤ x

Tactic:
intro d

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1
d : Set α
⊢ d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → s.sup f ≤ sSup d → ∃ x ∈ d, s.sup f ≤ x
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
s : Set α
⊢ s.Nonempty → SupClosed s → sSup s ∈ s

Tactic:
hne

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
s : Set α
hne : s.Nonempty
⊢ SupClosed s → sSup s ∈ s
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
x : M
⊢ ∀ (s : Set (Submodule R M)), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → R ∙ x ≤ sSup s → ∃ x_1 ∈ s, R ∙ x ≤ x_1

Tactic:
intro d

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
d : Set (Submodule R M)
⊢ d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → R ∙ x ≤ sSup d → ∃ x_1 ∈ d, R ∙ x ≤ x_1
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: case cons
α : Type u_1
t : Multiset α
a : α
s : Multiset α
ih : (s + t).antidiagonal = s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal
⊢ (a ::ₘ s + t).antidiagonal = (a ::ₘ s).antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal

Tactic:
simp_rw [cons_add, antidiagonal_cons, ih, add_bind, bind_map, map_bind, map_map]
    congr! <;> simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i = g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i

Tactic:
congr 2

Goal state after:
case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ ∏ i ∈ s \ {i}, g i = ∏ i ∈ s \ {i}, f i

case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ ∏ i ∈ s \ {i}, h i = ∏ i ∈ s \ {i}, f i
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ True ∧ f.range ≤ map f p ↔ Codisjoint p f.ker

Tactic:
true_and,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ f.range ≤ map f p ↔ Codisjoint p f.ker
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

Tactic:
by_cases hs : x ∈ s

Goal state after:
case pos
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : x ∈ s
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

case neg
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : ¬x ∈ s
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

Tactic:
by
  by_cases hs : x ∈ s <;> by_cases ht : x ∈ t <;> simp [mem_symmDiff, *]

Goal state after: