mathlib-initiative/mathlib-tactics huggingface dataset:
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
x✝¹ : M →+ M₂
x✝ : M
⊢ (0 • x✝¹) x✝ = 0 x✝

Tactic:
rw [DomMulAct.smul_addMonoidHom_apply]
    -- TODO there should be a simp lemma for `DomMulAct.mk.symm 0`
    simp [DomMulAct.mk, MulOpposite.opEquiv]

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

Goal state before:
pp: R : Type u_1
S : Type u_5
M₃ : Type u_11
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
⊢ f (x • 1) = g (x • 1)

Tactic:
f.map_smulₛₗ,

Goal state after:
R : Type u_1
S : Type u_5
M₃ : Type u_11
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
⊢ σ x • f 1 = g (x • 1)
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
f : M →+ M₂
⊢ ∀ ⦃a₂ : M →+ M₂⦄, f.toNatLinearMap = a₂.toNatLinearMap → f = a₂

Tactic:
g

Goal state after:
M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
f g : M →+ M₂
⊢ f.toNatLinearMap = g.toNatLinearMap → f = g
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
f : M →+ M₂
⊢ ∀ ⦃a₂ : M →+ M₂⦄, f.toIntLinearMap = a₂.toIntLinearMap → f = a₂

Tactic:
g

Goal state after:
M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
f g : M →+ M₂
⊢ f.toIntLinearMap = g.toIntLinearMap → f = g
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
⊢ f (MulOpposite.op x • 1) = g (MulOpposite.op x • 1)

Tactic:
f.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) • f 1 = g (MulOpposite.op x • 1)
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Surjective ⇑(f' ^ n)
⊢ Surjective ⇑f'

Tactic:
by
  rw [← Nat.succ_pred_eq_of_pos (Nat.pos_iff_ne_zero.mpr hn), pow_succ', coe_mul] at h
  exact Surjective.of_comp h

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
s : Set (Submodule R M)
t : R
m : M
h : m ∈ (sSup (toAddSubmonoid '' s)).toAddSubsemigroup
⊢ t • m ∈ (sSup (toAddSubmonoid '' s)).toAddSubsemigroup

Tactic:
AddSubmonoid.mem_toSubsemigroup,

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 ∈ sSup (toAddSubmonoid '' s)
⊢ t • m ∈ sSup (toAddSubmonoid '' s)
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: M : Type u_4
R : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N₁ N₂ : Submodule R M
⊢ Disjoint N₁ N₂ ↔ ∀ {x y : M}, x ∈ N₁ → y ∈ N₂ → x + y = 0 → x = 0 ∧ y = 0

Tactic:
by
  simp only [← Submodule.mem_toAddSubgroup, ← AddSubgroup.disjoint_iff_add_eq_zero]
  aesop (add norm [disjoint_def', AddSubgroup.disjoint_def'])

Goal state after:
Module: Mathlib.Algebra.Ring.CharZero

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hϕ : Injective ⇑ϕ
hR : CharZero R
⊢ Injective Nat.cast

Tactic:
intro a b h

Goal state after:
R : Type u_2
S : Type u_3
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hϕ : Injective ⇑ϕ
hR : CharZero R
a b : ℕ
h : ↑a = ↑b
⊢ a = b
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 σ₁₂
p : Submodule R M
f : M →ₛₗ[σ₁₂] M₂
hf : InjOn ⇑f ↑p
⊢ Injective ⇑(f.submoduleMap p)

Tactic:
intro ⟨x, hx⟩ ⟨y, hy⟩ hxy
  replace hxy : f x = f y := by simpa [Subtype.ext_iff] using hxy
  aesop

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 : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)

Tactic:
by simp [mem_iSup_of_directed hS]

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

Goal state before:
pp: case zero
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x : R) (hx : x ∈ s) (y : R) (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 ⋯
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
⊢ p x 0 hx ⋯

Tactic:
exact zero_right x hx

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)

Tactic:
by simp [mem_iSup_of_directed hS]

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

Goal state before:
pp: case zero
R : Type u
inst✝ : NonUnitalNonAssocRing 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 ⋯
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
⊢ p x 0 hx ⋯

Tactic:
exact zero_right x hx

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
a : A
m : M
⊢ ((algebraMap R A) r * a) • m = a • r • m

Tactic:
Algebra.commutes,

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
a : A
m : M
⊢ (a * (algebraMap R A) r) • m = a • r • m
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
inst✝¹ : NonUnitalNonAssocRing R
ι : Sort u_1
inst✝ : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)

Tactic:
by simp [mem_iSup_of_directed hS]

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
f g : A →ₐ[R] B
h : (fun f ↦ (↑↑f.toRingHom).toFun) f = (fun f ↦ (↑↑f.toRingHom).toFun) g
⊢ f = g

Tactic:
rcases f with ⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩
    rcases g with ⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩
    congr

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

Goal state before:
pp: case zero
R : Type u
inst✝ : NonAssocSemiring 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 ⋯
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
⊢ p x 0 hx ⋯

Tactic:
exact zero_right x hx

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

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
hx : x ∈ closure s
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

Tactic:
mem_closure_iff

Goal state after:
case mp
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
hx : x ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)

Tactic:
by simp [mem_iSup_of_directed hS]

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

Goal state before:
pp: case zero
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
⊢ p x 0 hx ⋯

Tactic:
exact zero_right x hx

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

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

Tactic:
mem_closure_iff

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)

Tactic:
by simp [mem_iSup_of_directed hS]

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬p ^ 2 ∣ b
⊢ p ∣ a

Tactic:
rcases hp.dvd_or_dvd ((dvd_pow_self p (Nat.succ_ne_zero n)).trans hpow) with H | hbdiv
  · exact hp.dvd_of_dvd_pow H
  obtain ⟨x, rfl⟩ := hp.dvd_of_dvd_pow hbdiv
  obtain ⟨y, hy⟩ := hpow
  -- Then we can divide out a common factor of `p ^ n` from the equation `hy`.
  have : a ^ n.succ * x ^ n = p * y := by
    refine mul_left_cancel₀ (pow_ne_zero n hp.ne_zero) ?_
    rw [← mul_assoc _ p, ← pow_succ, ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n),
      mul_assoc]
  -- So `p ∣ a` (and we're done) or `p ∣ x`, which can't be the case since it implies `p^2 ∣ b`.
  refine hp.dvd_of_dvd_pow ((hp.dvd_or_dvd ⟨_, this⟩).resolve_right fun hdvdx => hb ?_)
  obtain ⟨z, rfl⟩ := hp.dvd_of_dvd_pow hdvdx
  rw [pow_two, ← mul_assoc]
  exact dvd_mul_right _ _

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c d : M
h : a * b ~ᵤ c * d
h₁ : a ~ᵤ c
ha : a ≠ 0
u : Mˣ
hu : a * b * ↑u = c * d
v : Mˣ
hv : c * ↑v = a
⊢ c * ↑v * (b * ↑(u * v)) = c * (↑v * d)

Tactic:
mul_left_comm c,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c d : M
h : a * b ~ᵤ c * d
h₁ : a ~ᵤ c
ha : a ≠ 0
u : Mˣ
hu : a * b * ↑u = c * d
v : Mˣ
hv : c * ↑v = a
⊢ c * ↑v * (b * ↑(u * v)) = ↑v * (c * d)
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r : M₀
⊢ r ∈ M₀⁰ ↔ ∀ (x : M₀), r * x = 0 → x = 0

Tactic:
rw [← nonZeroDivisorsLeft_eq_nonZeroDivisors]; rfl

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

Goal state before:
pp: case mp
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ (∃ x, x * Associates.mk a = 0 ∧ x ≠ 0) → ∃ x, x * a = 0 ∧ x ≠ 0

Tactic:
rintro ⟨⟨x⟩, hx₁, hx₂⟩
    refine ⟨x, ?_, ?_⟩
    · rwa [← Associates.mk_eq_zero, ← Associates.mk_mul_mk, ← Associates.quot_mk_eq_mk]
    · rwa [← Associates.mk_ne_zero, ← Associates.quot_mk_eq_mk]

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

Goal state before:
pp: M : Type u_1
inst✝ : MonoidWithZero M
⊢ Associates.mk (Quot.out 0) = 0

Tactic:
quot_out

Goal state after:
M : Type u_1
inst✝ : MonoidWithZero M
⊢ 0 = 0
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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₂
q : Submodule R₂ M₂
h : q ≤ f.range
⊢ map f (comap f q) = q

Tactic:
by
  rwa [Submodule.map_comap_eq, inf_eq_right]

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

Goal state before:
pp: case mpr
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
⊢ (∃ y ∈ f.range, ⇑f ⁻¹' {y} ⊆ ↑p) → f.ker ≤ p

Tactic:
· rintro ⟨y, h₁, h₂⟩
    rw [SetLike.le_def]
    intro z hz
    simp only [mem_ker] at hz
    rw [← SetLike.mem_coe, coe_range, Set.mem_range] at h₁
    obtain ⟨x, hx⟩ := h₁
    have hx' : x ∈ p := h₂ hx
    have hxz : z + x ∈ p := by
      apply h₂
      simp [hx, hz]
    suffices z + x - x ∈ p by simpa only [this, add_sub_cancel_right]
    exact p.sub_mem hxz hx'

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
h : ∀ (x y z : α), x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z
x✝ y z : α
xz : x✝ ≤ z
⊢ (x✝ ⊔ y) ⊓ z ≤ x✝ ⊔ y ⊓ z

Tactic:
rw [← inf_eq_left.2 xz, h]

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
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : x ∈ span R s
⊢ p x hx

Tactic:
by
  have key {v} : v ∈ span R s ↔ v ∈ closure (@univ R • s) := by simp [← span_eq_closure]
  refine AddSubmonoid.closure_induction (motive := fun x hx ↦ p x (key.mpr hx))
    ?_ zero (by simpa only [key] using add) (key.mp hx)
  rintro - ⟨r, -, x, hx, rfl⟩
  exact smul_mem r x hx

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : Frame α
f : ι → α
ha : IsAtom ⊥
h : ⊥ ≤ ⨆ i, f i
ha' : ∀ (i : ι), ¬⊥ ≤ f i
ha'' : Disjoint ⊥ (⨆ i, f i)
⊢ False

Tactic:
exact ha.1 rfl

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderTop α
a b : α
ha : IsCoatom a
⊢ ¬Codisjoint a b ↔ b ≤ a

Tactic:
rw [codisjoint_iff, ← sup_eq_left]

Goal state after:
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderTop α
a b : α
ha : IsCoatom a
⊢ ¬a ⊔ b = ⊤ ↔ a ⊔ b = a
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Set α
t : Set β
⊢ supClosure s ×ˢ supClosure t ⊆ supClosure (s ×ˢ t)

Tactic:
by
      rintro ⟨_, _⟩ ⟨⟨u, hu, hus, rfl⟩, v, hv, hvt, rfl⟩
      refine ⟨u ×ˢ v, hu.product hv, ?_, ?_⟩
      · simpa only [coe_product] using Set.prod_mono hus hvt
      · simp [prodMk_sup'_sup']

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝² : PartialOrder α✝
α : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : IsStronglyCoatomic α
⊢ IsStronglyAtomic αᵒᵈ

Tactic:
rwa [isStronglyAtomic_dual_iff_is_stronglyCoatomic]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
⊢ x = y ↔ ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)

Tactic:
by
  refine ⟨fun h => h ▸ by simp, fun h => ?_⟩
  exact le_antisymm (le_iff_atom_le_imp.2 fun a ha hx => (h a ha).1 hx)
    (le_iff_atom_le_imp.2 fun a ha hy => (h a ha).2 hy)

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
b : α
s : Set α
hsb : IsLUB s b
hs : ∀ a ∈ s, IsAtom a
a : α
ha : a ∈ s
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
· exact Or.inr ⟨a, hs _ ha, hsb.1 ha⟩

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : IsCoatomistic α
b : α
s : Set α
hsb : IsGLB s b
hs : ∀ a ∈ s, IsCoatom a
a : α
ha : a ∈ s
⊢ b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a

Tactic:
· exact Or.inr ⟨a, hs _ ha, hsb.1 ha⟩

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → α
hs : s.SupIndep f
ht : t.SupIndep f
h : Disjoint (s.sup f) (t.sup f)
⊢ (s ∪ t).SupIndep f

Tactic:
rw [show s ∪ t = ({s, t} : Finset _).biUnion id by simp]

Goal state after:
α : Type u_1
ι : Type u_3
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → α
hs : s.SupIndep f
ht : t.SupIndep f
h : Disjoint (s.sup f) (t.sup f)
⊢ ({s, t}.biUnion id).SupIndep f
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mpr.inl
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
j k : ι
hij : k ≠ j
huniv : ∀ (k_1 : ι), k_1 = k ∨ k_1 = j
h : Disjoint (t k) (t j)
⊢ Disjoint (t k) (⨆ j, ⨆ (_ : j ≠ k), t j)

Tactic:
refine h.mono_right (iSup_le fun i => iSup_le fun hi => Eq.le ?_)
      rw [(huniv i).resolve_left hi]

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

Goal state before:
pp: case mpr
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s
s : Set α
hs : k ≤ sSup s
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

Tactic:
obtain ⟨t, ht⟩ :=
        H s Subtype.val
          (by
            delta iSup
            rwa [Subtype.range_coe])

Goal state after:
case mpr
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s
s : Set α
hs : k ≤ sSup s
t : Finset ↑s
ht : k ≤ t.sup Subtype.val
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
h : ¬a ∈ s
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a

Tactic:
· exact Or.inl (mulIndicator_of_notMem h f)

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
rw [le_iff_compact_le_imp]

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ ∀ (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: case refine_3
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
⊢ ∀ (a : R), ∀ x ∈ span R s, x • y ∈ span R (s • t) → (a • x) • y ∈ span R (s • t)

Tactic:
intro r s0 _ hy; rw [IsScalarTower.smul_assoc]; exact smul_mem _ r hy

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

Goal state before:
pp: case mpr.smul
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
a : R
x : M
hx : x ∈ span R S
hx' : f ⟨x, hx⟩ = g ⟨x, hx⟩
⊢ f ⟨a • x, ⋯⟩ = g ⟨a • x, ⋯⟩

Tactic:
f.map_smul a ⟨x, hx⟩,

Goal state after:
case mpr.smul
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
a : R
x : M
hx : x ∈ span R S
hx' : f ⟨x, hx⟩ = g ⟨x, hx⟩
⊢ a • f ⟨x, hx⟩ = g ⟨a • x, ⋯⟩
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
⊢ a ⊓ sSup s ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id

Tactic:
rw [le_iff_compact_le_imp]

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
⊢ ∀ (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id