mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
x y : M
⊢ x - y ∈ f.ker ↔ f x = f y

Tactic:
mem_ker,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
x y : M
⊢ f (x - y) = 0 ↔ f x = f y
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✝¹ x✝ : ULift.{?u.15, v} M
⊢ x✝² • (x✝¹ * x✝) = x✝² • x✝¹ * x✝² • x✝

Tactic:
ext
      simp [smul_mul']

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p q : Submodule R M
h : p ⋖ q
P : Submodule R₂ M₂
h₁ : map f p < P
h₂ : P < map f q
⊢ map f p < map f (comap f P)

Tactic:
refine h₁.trans_le ?_

Goal state after:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p q : Submodule R M
h : p ⋖ q
P : Submodule R₂ M₂
h₁ : map f p < P
h₂ : P < map f q
⊢ P ≤ map f (comap f P)
Module: Mathlib.Algebra.Ring.Subsemiring.Defs

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike S R
inst✝¹ : AddSubmonoidWithOneClass S R
s : S
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑(OfNat.ofNat n) ∈ s

Tactic:
exact natCast_mem s n

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

Goal state before:
pp: ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ IsMulCommutative ↥(⨆ i, S i)

Tactic:
refine .of_setLike_mul_comm ?_
  simp_rw [← SetLike.mem_coe, coe_iSup_of_directed dir, Set.mem_iUnion,
    SetLike.mem_coe, forall_exists_index]
  intro a i ha b j hb
  obtain ⟨k, hik, hjk⟩ := dir i j
  exact setLike_mul_comm (hik ha) (hjk hb)

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

Goal state before:
pp: R : Type u
inst✝¹ : NonUnitalNonAssocSemiring R
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ IsMulCommutative ↥(⨆ i, S i)

Tactic:
refine .of_setLike_mul_comm ?_
  simp_rw [← SetLike.mem_coe, coe_iSup_of_directed dir, Set.mem_iUnion,
    SetLike.mem_coe, forall_exists_index]
  intro a i ha b j hb
  obtain ⟨k, hik, hjk⟩ := dir i j
  exact setLike_mul_comm (hik ha) (hjk hb)

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
r : R
m : M
⊢ (r • 1) • m = (algebraMap R A) r • 1 • m

Tactic:
Algebra.smul_def,

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
r : R
m : M
⊢ ((algebraMap R A) r * 1) • m = (algebraMap R A) r • 1 • m
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝¹¹ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁰ : Semiring A✝
inst✝⁹ : Algebra R✝ A✝
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module A✝ M
inst✝⁶ : Module R✝ M
inst✝⁵ : IsScalarTower R✝ A✝ M
R : Type u_4
S : Type u_5
A : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Algebra S A
r : R
s : S
a : A
⊢ r • s • a = s • r • a

Tactic:
Algebra.smul_def,

Goal state after:
R✝ : Type u_1
inst✝¹¹ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁰ : Semiring A✝
inst✝⁹ : Algebra R✝ A✝
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module A✝ M
inst✝⁶ : Module R✝ M
inst✝⁵ : IsScalarTower R✝ A✝ M
R : Type u_4
S : Type u_5
A : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Algebra S A
r : R
s : S
a : A
⊢ (algebraMap R A) r * s • a = s • r • a
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
hf : f 1 = 1
r : R
h : Invertible ((algebraMap R A) r)
⊢ f (r • ⅟((algebraMap R A) r)) = 1

Tactic:
Algebra.smul_def,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
hf : f 1 = 1
r : R
h : Invertible ((algebraMap R A) r)
⊢ f ((algebraMap R A) r * ⅟((algebraMap R A) r)) = 1
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Injective ⇑b
x y : F
e : (algebraMap F E) x = (algebraMap F E) y
⊢ x • b 1 = y • b 1

Tactic:
Algebra.smul_def,

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Injective ⇑b
x y : F
e : (algebraMap F E) x = (algebraMap F E) y
⊢ (algebraMap F E) x * b 1 = y • b 1
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Injective ⇑b
x y : F
e : (algebraMap F E) x = (algebraMap F E) y
⊢ (algebraMap F E) x * b 1 = y • b 1

Tactic:
Algebra.smul_def,

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Injective ⇑b
x y : F
e : (algebraMap F E) x = (algebraMap F E) y
⊢ (algebraMap F E) x * b 1 = (algebraMap F E) y * b 1
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b : M
⊢ a ∣ p * b → p ∣ a ∨ a ∣ b

Tactic:
by
  rintro ⟨c, hc⟩
  rcases hp.2.2 a c (hc ▸ dvd_mul_right _ _) with (h | ⟨x, rfl⟩)
  · exact Or.inl h
  · rw [mul_left_comm, mul_right_inj' hp.ne_zero] at hc
    exact Or.inr (hc.symm ▸ dvd_mul_right _ _)

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 r
h' : p ~ᵤ q
⊢ DvdNotUnit q r

Tactic:
by
  obtain ⟨u, rfl⟩ := h'.symm
  obtain ⟨hp, x, hx⟩ := h
  have hq : q ≠ 0 := by simp_all
  refine ⟨hq, x * u, mt isUnit_of_mul_isUnit_left hx.1, ?_⟩
  rw [mul_comm x, ← mul_assoc, ← hx.2]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : R
⊢ e.symm (e 1 * (algebraMap R A) x) = e.symm (x • e 1)

Tactic:
Algebra.smul_def,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : R
⊢ e.symm (e 1 * (algebraMap R A) x) = e.symm ((algebraMap R A) x * e 1)
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ (algebraMap R A) (e.symm (e 1 * x)) * e.symm 1 • e 1 = x

Tactic:
Algebra.smul_def,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ (algebraMap R A) (e.symm (e 1 * x)) * ((algebraMap R A) (e.symm 1) * e 1) = x
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: case mp
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass R S M
r : S
x : M
hx : x ∈ {r} • N
⊢ ∃ m ∈ N, x = r • m

Tactic:
induction x, hx using Submodule.set_smul_inductionOn with
    | smul₀ => aesop
    | @smul₁ t n mem h =>
      rcases h with ⟨n, hn, rfl⟩
      exact ⟨t • n, by aesop, smul_comm _ _ _⟩
    | add mem₁ mem₂ h₁ h₂ =>
      rcases h₁ with ⟨m₁, h₁, rfl⟩
      rcases h₂ with ⟨m₂, h₂, rfl⟩
      exact ⟨m₁ + m₂, Submodule.add_mem _ h₁ h₂, by simp⟩
    | zero => exact ⟨0, Submodule.zero_mem _, by simp⟩

Goal state after:
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
⊢ 0 ∈ ↑(span R s)

Tactic:
simp only [SetLike.mem_coe, Submodule.zero_mem]

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

Goal state before:
pp: case refine_1.inl
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
h✝ : x ∈ span R (↑p ∪ ↑p')
y : M
h : y ∈ ↑p
⊢ ∃ y_1 ∈ p, ∃ z ∈ p', y_1 + z = y

Tactic:
exact ⟨y, h, 0, by simp, by simp⟩

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
c : α
hc : c ∈ s
d : α
hd : d ∈ s
hcd : ⟨c, hc⟩ < ⟨d, hd⟩
x : α
hcx : c ⋖ x
hxd : x ≤ d
⊢ ⟨c, hc⟩ < ⟨x, ⋯⟩

Tactic:
simpa
        using! hcx.lt

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : Lattice α
s : Set α
p : (a : α) → a ∈ latticeClosure s → Prop
mem : ∀ (a : α) (has : a ∈ s), p a ⋯
sup : ∀ (a : α) (has : a ∈ latticeClosure s) (b : α) (hbs : b ∈ latticeClosure s), p a has → p b hbs → p (a ⊔ b) ⋯
inf : ∀ (a : α) (has : a ∈ latticeClosure s) (b : α) (hbs : b ∈ latticeClosure s), p a has → p b hbs → p (a ⊓ b) ⋯
a✝ : α
has : a✝ ∈ latticeClosure s
h : IsSublattice {a | ∃ (has : a ∈ latticeClosure s), p a has}
a : α
ha : a ∈ s
⊢ a ∈ {a | ∃ (has : a ∈ latticeClosure s), p a has}

Tactic:
exact ⟨subset_latticeClosure ha, mem a ha⟩

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

Goal state before:
pp: case refine_1.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
x : M
hx : x ∈ S
⊢ x ∈ span R ↑{x}

Tactic:
Finset.coe_singleton

Goal state after:
case refine_1.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
x : M
hx : x ∈ S
⊢ x ∈ R ∙ x
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
⊢ iSupIndep f ↔ Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 2 ⊔ f 0) ∧ Disjoint (f 2) (f 0 ⊔ f 1)

Tactic:
by
  rw [iSupIndep_def, sup_comm (f 2) (f 0)]
  refine ⟨fun h ↦ ⟨?_, ?_, ?_⟩, fun ⟨h₀, h₁, h₂⟩ i ↦ ?_⟩
  · simpa using h 0
  · simpa using h 1
  · simpa using h 2
  · fin_cases i <;> simpa

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case e'_5
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ ⨆ j, ⨆ (_ : j ≠ ⟨a, b⟩), (f ∘ Subtype.val) j = ⨆ a_1 ∈ s.erase a, f a_1

Tactic:
refine iSup_subtype.trans ?_

Goal state after:
case e'_5
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ ⨆ i, ⨆ (h : i ∈ s), ⨆ (_ : ⟨i, h⟩ ≠ ⟨a, b⟩), (f ∘ Subtype.val) ⟨i, h⟩ = ⨆ a_1 ∈ s.erase a, f a_1
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
A : Type w
M : Type v₁
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : MulAction A M
inst✝ : SMul R M
h : ∀ (r : R) (x : M), (algebraMap R A) r • x = r • x
r : R
a : A
x : M
⊢ (r • a) • x = r • a • x

Tactic:
Algebra.smul_def,

Goal state after:
R : Type u
A : Type w
M : Type v₁
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : MulAction A M
inst✝ : SMul R M
h : ∀ (r : R) (x : M), (algebraMap R A) r • x = r • x
r : R
a : A
x : M
⊢ ((algebraMap R A) r * a) • x = r • a • x
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : Algebra R A
h : ∀ (x : R), (algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)
x : R
y : S
z : A
⊢ (x • y) • z = x • y • z

Tactic:
Algebra.smul_def,

Goal state after:
R : Type u
S : Type v
A : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : Algebra R A
h : ∀ (x : R), (algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)
x : R
y : S
z : A
⊢ (algebraMap S A) ((algebraMap R S) x * y) * z = (algebraMap R A) x * ((algebraMap S A) y * z)
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
inst✝¹ : One M
h : M → β
f : α → M
s : Set α
x : α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ h (s.mulIndicator f x) = s.piecewise (h ∘ f) (const α (h 1)) x

Tactic:
let := Classical.decPred (· ∈ s)

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝¹ : One M
h : M → β
f : α → M
s : Set α
x : α
inst✝ : DecidablePred fun x ↦ x ∈ s
this : DecidablePred fun x ↦ x ∈ s := Classical.decPred fun x ↦ x ∈ s
⊢ h (s.mulIndicator f x) = s.piecewise (h ∘ f) (const α (h 1)) x
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
inst✝¹ : One M
h : M → β
f : α → M
s : Set α
x : α
inst✝ : DecidablePred fun x ↦ x ∈ s
this : DecidablePred fun x ↦ x ∈ s := Classical.decPred fun x ↦ x ∈ s
⊢ h (s.mulIndicator f x) = s.piecewise (h ∘ f) (const α (h 1)) x

Tactic:
convert! s.apply_piecewise f (const α 1) (fun _ => h) (x := x) using 2

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

Goal state before:
pp: R : Type u_8
M : Type u_9
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
x y : M
⊢ R ∙ x = R ∙ y ↔ ∃ z, z • x = y

Tactic:
constructor
  · simp only [le_antisymm_iff, span_singleton_le_iff_mem, mem_span_singleton]
    rintro ⟨⟨a, rfl⟩, b, hb⟩
    rcases eq_or_ne y 0 with rfl | hy; · simp
    refine ⟨⟨b, a, ?_, ?_⟩, hb⟩
    · apply smul_left_injective R hy
      simpa only [mul_smul, one_smul]
    · rw [← hb] at hy
      apply smul_left_injective R (smul_ne_zero_iff.1 hy).2
      simp only [mul_smul, one_smul, hb]
  · rintro ⟨u, rfl⟩
    exact (span_singleton_group_smul_eq _ _ _).symm

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set (Set α)
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, sSupIndep a
⊢ sSupIndep (⋃ i, ↑i)

Tactic:
exact sSupIndep_iUnion_of_directed hs.directed_val (by simpa using h)

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
u : Finset α
hu : ↑u ⊆ range fun x ↦ f ↑x
t : Set ι
ht : t ⊆ s
ht' : t.Finite
htu : u.sup id = ⨆ i ∈ t, f i
⊢ u.sup id ⊓ a = ⊥

Tactic:
← disjoint_iff,

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
u : Finset α
hu : ↑u ⊆ range fun x ↦ f ↑x
t : Set ι
ht : t ⊆ s
ht' : t.Finite
htu : u.sup id = ⨆ i ∈ t, f i
⊢ Disjoint (u.sup id) a
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s✝ t : Set M
s : Submodule R M
x : M
left✝ : x ∈ ↑s
ht : R ∙ x ∈ (fun x ↦ R ∙ x) '' ↑s
⊢ IsCompactElement (R ∙ x)

Tactic:
apply singleton_span_isCompactElement

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

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Multiset ι
f g : ι → R
⊢ (map (fun i ↦ f i + g i) 0).prod = (map (fun p ↦ (map f p.1).prod * (map g p.2).prod) (antidiagonal 0)).sum

pp: case refine_2
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s✝ : Multiset ι
f g : ι → R
a : ι
s : Multiset ι
ih : (map (fun i ↦ f i + g i) s).prod = (map (fun p ↦ (map f p.1).prod * (map g p.2).prod) s.antidiagonal).sum
⊢ (map (fun i ↦ f i + g i) (a ::ₘ s)).prod =
    (map (fun p ↦ (map f p.1).prod * (map g p.2).prod) (a ::ₘ s).antidiagonal).sum

Tactic:
· simp only [map_zero, prod_zero, antidiagonal_zero, map_singleton, mul_one, sum_singleton]

Goal state after:
case refine_2
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s✝ : Multiset ι
f g : ι → R
a : ι
s : Multiset ι
ih : (map (fun i ↦ f i + g i) s).prod = (map (fun p ↦ (map f p.1).prod * (map g p.2).prod) s.antidiagonal).sum
⊢ (map (fun i ↦ f i + g i) (a ::ₘ s)).prod =
    (map (fun p ↦ (map f p.1).prod * (map g p.2).prod) (a ::ₘ s).antidiagonal).sum
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
p p' : Submodule R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
xx : M
yy : M'
hxx : xx ∈ p ⊔ p'
⊢ yy ∈ q₁ ⊔ q₁' → (xx, yy) ∈ p.prod q₁ ⊔ p'.prod q₁'

Tactic:
hyy

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
p p' : Submodule R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
xx : M
yy : M'
hxx : xx ∈ p ⊔ p'
hyy : yy ∈ q₁ ⊔ q₁'
⊢ (xx, yy) ∈ p.prod q₁ ⊔ p'.prod q₁'
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c✝ : α
hbc : b ≤ c✝
h : sSup {a | a ≤ c✝ ∧ IsAtom a} = c✝
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c✝}
hc2 : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
⊢ ∀ ⦃b_1 : α⦄, b_1 ∈ sSup '' c → Disjoint b b_1

Tactic:
rintro _ ⟨s, hs, rfl⟩

Goal state after:
case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c✝ : α
hbc : b ≤ c✝
h : sSup {a | a ≤ c✝ ∧ IsAtom a} = c✝
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c✝}
hc2 : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
s : Set α
hs : s ∈ c
⊢ Disjoint b (sSup s)
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case mp
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
hx : x ∈ p
y : M
hy : y ∈ s
z : M
hz : z ∈ t
hyzx : y + z = x
⊢ z ∈ p

Tactic:
← add_right_inj,

Goal state after:
case mp
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
hx : x ∈ p
y : M
hy : y ∈ s
z : M
hz : z ∈ t
hyzx✝ : y + z = x
hyzx : ?mp.a + (y + z) = ?mp.a + x
⊢ z ∈ p

case mp.a
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
hx : x ∈ p
y : M
hy : y ∈ s
z : M
hz : z ∈ t
hyzx : y + z = x
⊢ M
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
x : α
ha : x ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
hx : x ∈ s ∨ x = x
⊢ Disjoint x (sSup (s \ {x}))

Tactic:
exact con.mono_right ((sSup_le_sSup Set.sdiff_subset).trans le_sup_right)

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

Goal state before:
pp: case inr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))

Tactic:
· have h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a} := by
        simp only [Set.union_singleton]
        rw [Set.insert_sdiff_of_notMem]
        rw [Set.mem_singleton_iff]
        exact Ne.symm xa
      rw [h, sSup_union, sSup_singleton]
      apply
        (s_ind (hx.resolve_right xa)).disjoint_sup_right_of_disjoint_sup_left
          (a_dis_Sup_s.mono_right _).symm
      rw [← sSup_insert, Set.insert_sdiff_singleton, Set.insert_eq_of_mem (hx.resolve_right xa)]

Goal state after:
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Injective e
a b : α →₀ M
h : mapRange e he₀ a = mapRange e he₀ b
⊢ a = b

Tactic:
Finsupp.ext_iff

Goal state after:
α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Injective e
a b : α →₀ M
h : ∀ (a_1 : α), (mapRange e he₀ a) a_1 = (mapRange e he₀ b) a_1
⊢ ∀ (a_1 : α), a a_1 = b a_1
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✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
s : Set M
f g : M →ₛₗ[σ₁₂] M₂
⊢ Set.EqOn ⇑f ⇑g ↑(span R s) ↔ Set.EqOn (⇑f) (⇑g) s

Tactic:
rw [← le_eqLocus, span_le]; rfl

Goal state after:
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
⊢ Nontrivial (α →₀ M) → Nonempty α ∧ Nontrivial M

Tactic:
rintro ⟨f, g, hfg⟩

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f g : α →₀ M
hfg : f ≠ g
⊢ Nonempty α ∧ Nontrivial M
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
P : Type u_11
inst✝² : AddZeroClass M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
g : N →+ P
f : α → M →+ N
a : α
⊢ (g.comp (liftAddHom f)).comp (singleAddHom a) = g.comp (f a)

Tactic:
AddMonoidHom.comp_assoc,

Goal state after:
α : Type u_1
M : Type u_8
N : Type u_10
P : Type u_11
inst✝² : AddZeroClass M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
g : N →+ P
f : α → M →+ N
a : α
⊢ g.comp ((liftAddHom f).comp (singleAddHom a)) = g.comp (f a)
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset

Goal state before:
pp: R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
s : Multiset ι
f g : ι → R
h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i
h : ∀ (i : ι), i ∈ s → f i ≤ g i
⊢ (map f s).prod ≤ (map g s).prod

Tactic:
cases s using Quotient.ind
  simp only [quot_mk_to_coe, mem_coe, map_coe, prod_coe] at *
  apply List.prod_map_le_prod_map₀ f g h0 h

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
s : Multiset (α →₀ M)
a : α
h : a ∈ (Multiset.sum 0).support
⊢ False

Tactic:
by simp at h

Goal state after: