mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝⁴ : FunLike F α β
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
f g : FrameHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝⁴ : FunLike F α β
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
g : FrameHom α β
toFun✝ : α → β
map_inf'✝ : ∀ (a b : α), toFun✝ (a ⊓ b) = toFun✝ a ⊓ toFun✝ b
map_top'✝ : { toFun := toFun✝, map_inf' := map_inf'✝ }.toFun ⊤ = ⊤
map_sSup'✝ :
  ∀ (s : Set α),
    { toFun := toFun✝, map_inf' := map_inf'✝, map_top' := map_top'✝ }.toFun (sSup s) =
      sSup ({ toFun := toFun✝, map_inf' := map_inf'✝, map_top' := map_top'✝ }.toFun '' s)
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, map_inf' := map_inf'✝, map_top' := map_top'✝, map_sSup' := map_sSup'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_inf' := map_inf'✝, map_top' := map_top'✝, map_sSup' := map_sSup'✝ } = g
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✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ x ∈ p, f x ∈ q
⊢ (f.domRestrict p).ker = comap p.subtype f.ker

Tactic:
ker_domRestrict

Goal state after:
R : Type u_1
R₂ : Type u_2
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₂
p : Submodule R M
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ x ∈ p, f x ∈ q
⊢ comap p.subtype f.ker = comap p.subtype f.ker
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
⊢ ∀ (x : G₀ˣ), (∀ (g : G₀ˣ), g * x = x * g) → ∀ (g : G₀), g * ↑x = ↑x * g

Tactic:
intro u

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
⊢ (∀ (g : G₀ˣ), g * u = u * g) → ∀ (g : G₀), g * ↑u = ↑u * g
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)
⊢ x✝¹ * x✝ * ↑(n + 1) = x✝¹ * (x✝ * ↑(n + 1))

Tactic:
rw [Nat.cast_succ, mul_add, ihn, mul_add, mul_add, mul_one, mul_one]

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

Goal state before:
pp: case mem
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝ : R
hx : x✝ ∈ s
⊢ x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
| mem _ hx =>

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

Goal state before:
pp: case mem
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝ : R
hx : x✝ ∈ ↑(Subsemigroup.closure s)
⊢ x✝ ∈ closure s

Tactic:
| mem _ 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:
smul_smul,

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

Tactic:
by
  rw [← mul_one x, ← mul_one y, ← smul_eq_mul, ← smul_eq_mul,
    map_smul, map_smul, Algebra.smul_def, Algebra.smul_def, e]

Goal state after:
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 : Surjective ⇑b
x y z : F
hz : b z = 1
hy : x • y • 1 = b x
⊢ (algebraMap F E) (x * y) = b x

Tactic:
smul_smul,

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 : Surjective ⇑b
x y z : F
hz : b z = 1
hy : (x * y) • 1 = b x
⊢ (algebraMap F E) (x * y) = b x
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
hf : Function.Surjective ⇑f
t : Subsemiring S
⊢ t ≤ f.rangeS

Tactic:
by simp [hf]

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

Goal state before:
pp: case mem
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝ : R
hx : x✝ ∈ s
⊢ x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
| mem _ hx =>

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

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

Tactic:
| mem _ hx =>

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
c : M
ih : p ^ n ∣ a * (p ^ n * c) → p ^ n ∣ p ^ n * c
h' : p ^ (n + 1) ∣ a * (p ^ n * c)
⊢ p ^ n * p ∣ p ^ n * (a * c)

Tactic:
← pow_succ,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
c : M
ih : p ^ n ∣ a * (p ^ n * c) → p ^ n ∣ p ^ n * c
h' : p ^ (n + 1) ∣ a * (p ^ n * c)
⊢ p ^ (n + 1) ∣ p ^ n * (a * c)
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
⊢ p ^ n * (a ^ n.succ * x ^ n) = p ^ n * p * y

Tactic:
← pow_succ,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
⊢ p ^ n * (a ^ n.succ * x ^ n) = p ^ (n + 1) * y
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p₁ p₂ : M
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂

Tactic:
have : p₁ ∣ p₂ ^ k₂ := by
    rw [← h.dvd_iff_dvd_right]
    apply dvd_pow_self _ hk₁.ne'
  rw [← hp₁.dvd_prime_iff_associated hp₂]
  exact hp₁.dvd_of_dvd_pow this

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
hf : Function.Surjective ⇑f
t : Subring S
⊢ t ≤ f.range

Tactic:
by simp [hf]

Goal state after:
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

pp: case mp.mk.refine_2
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 ≠ 0

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

Goal state after:
case mp.mk.refine_2
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 ≠ 0
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₁
inst✝⁵ : Module S M₂
inst✝⁴ : SMulCommClass S R M₁
inst✝³ : SMulCommClass S R M₂
inst✝² : SMul R S
inst✝¹ : IsScalarTower R S M₁
inst✝ : IsScalarTower R S M₂
e : M₁ ≃ₗ[S] M₂
x✝ : R
⊢ e.conjRingEquiv.toFun ((algebraMap R (Module.End S M₁)) x✝) = (algebraMap R (Module.End S M₂)) x✝

Tactic:
ext; change e.restrictScalars R _ = _; 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
G : Type u_9
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
g : G
x : M
⊢ x = g⁻¹ • g • x

Tactic:
exact (inv_smul_smul g x).symm

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case sup
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure s,
    ∀ b ∈ latticeClosure s,
      a ∈ f ⁻¹' latticeClosure (f '' s) → b ∈ f ⁻¹' latticeClosure (f '' s) → a ⊔ b ∈ f ⁻¹' latticeClosure (f '' s)

pp: case left.inf
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure s,
    ∀ b ∈ latticeClosure s,
      a ∈ f ⁻¹' latticeClosure (f '' s) → b ∈ f ⁻¹' latticeClosure (f '' s) → a ⊓ b ∈ f ⁻¹' latticeClosure (f '' s)

pp: case right.mem
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ f '' s, a ∈ f '' latticeClosure s

pp: case sup
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊔ b ∈ f '' latticeClosure s

pp: case right.inf
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊓ b ∈ f '' latticeClosure s

Tactic:
· rintro a - b - ha hb
    simpa [map_sup] using isSublattice_latticeClosure.supClosed ha hb

Goal state after:
case left.inf
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure s,
    ∀ b ∈ latticeClosure s,
      a ∈ f ⁻¹' latticeClosure (f '' s) → b ∈ f ⁻¹' latticeClosure (f '' s) → a ⊓ b ∈ f ⁻¹' latticeClosure (f '' s)

case right.mem
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ f '' s, a ∈ f '' latticeClosure s

case sup
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊔ b ∈ f '' latticeClosure s

case right.inf
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊓ b ∈ f '' latticeClosure s
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
hi : t i = ⊥
⊢ Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)

Tactic:
simp [hi]

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

Goal state before:
pp: α : 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 α := {x | ∃ t, ↑t ⊆ s ∧ x = t.sup id}
dir_US : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
⊢ sSup s ≤ sSup S

Tactic:
apply sSup_le_sSup

Goal state after:
α : 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
⊢ s ⊆ S
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
this : t j ≤ ⨆ k, ⨆ (_ : k ≠ i), t k
⊢ t j = ⊥

Tactic:
replace ht := (ht i).mono_right this

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
this : t j ≤ ⨆ k, ⨆ (_ : k ≠ i), t k
ht : Disjoint (t i) (t j)
⊢ t j = ⊥
Module: Mathlib.Order.CompactlyGenerated.Basic

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

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

Tactic:
· intro H ι s hs
      obtain ⟨t, ht, ht'⟩ := H (Set.range s) hs
      have : ∀ x : t, ∃ i, s i = x := fun x => ht x.prop
      choose f hf using this
      refine ⟨Finset.univ.image f, ht'.trans ?_⟩
      rw [Finset.sup_le_iff]
      intro b hb
      rw [← show s (f ⟨b, hb⟩) = id b from hf _]
      exact Finset.le_sup (Finset.mem_image_of_mem f <| Finset.mem_univ (Subtype.mk b hb))

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : β → M
g : α → β
hg : Injective g
x : α
⊢ (g ⁻¹' g '' s).mulIndicator (f ∘ g) x = s.mulIndicator (f ∘ g) x

Tactic:
preimage_image_eq _ hg

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : β → M
g : α → β
hg : Injective g
x : α
⊢ s.mulIndicator (f ∘ g) x = s.mulIndicator (f ∘ g) x
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s = t.sup id
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

Tactic:
use t, hts

Goal state after:
case right
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s = t.sup id
⊢ k ≤ t.sup id
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ ∏ x ∈ s, f x = 0 ↔ ∃ a ∈ s, f a = 0

Tactic:
induction s using Finset.induction_on with

Goal state after:
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 ht

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 α
ht : ↑t ⊆ ⋃ i, s i
⊢ sSupIndep ↑t
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
⊢ ∀ (i : Finset α), (↑i ⊆ range fun x ↦ f ↑x) → a ⊓ i.sup id = ⊥

Tactic:
intro u

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 α
⊢ (↑u ⊆ range fun x ↦ f ↑x) → a ⊓ u.sup id = ⊥
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: F : Type u_8
α : Type u_9
β : Type u_10
ι : Type u_11
inst✝⁴ : FunLike F α β
inst✝³ : CommMonoid β
inst✝² : CommMonoid F
inst✝¹ : IsOneApply F α β
inst✝ : IsMulApply F α β
s : Finset ι
f : ι → F
x : α
⊢ (∏ i ∈ s, f i) x = ∏ i ∈ s, (f i) x

Tactic:
induction s using Finset.induction_on with

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
ι : Sort u_8
p : ι → Submodule R M
motive : M → Prop
x : M
hx : x ∈ ⨆ i, p i
mem : ∀ (i : ι), ∀ x ∈ p i, motive x
zero : motive 0
add : ∀ (x y : M), motive x → motive y → motive (x + y)
⊢ motive x

Tactic:
rw [← mem_toAddSubmonoid, iSup_toAddSubmonoid] at hx
  exact AddSubmonoid.iSup_induction (x := x) _ hx mem zero add

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

Goal state before:
pp: case inr.refine_1
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
I : α
a✝ : I ∈ S
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub

Tactic:
by_cases hS : S.Nonempty

Goal state after:
case pos
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : S.Nonempty
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub

case neg
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : ¬S.Nonempty
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub
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'
hyy : yy ∈ q₁ ⊔ q₁'
⊢ (xx, yy) ∈ p.prod q₁ ⊔ p'.prod q₁'

Tactic:
rcases mem_sup.1 hxx with ⟨x, hx, x', hx', rfl⟩

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'
yy : M'
hyy : yy ∈ q₁ ⊔ q₁'
x : M
hx : x ∈ p
x' : M
hx' : x' ∈ p'
hxx : x + x' ∈ p ⊔ p'
⊢ (x + x', yy) ∈ p.prod q₁ ⊔ p'.prod q₁'
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
R✝ : Type u_8
M✝ : Type u_9
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u_10
M : Type u_11
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝⁴ x✝³ x✝² : Submodule R M
hxy : x✝⁴ ≤ x✝²
x✝¹ : M
x✝ : x✝¹ ∈ (x✝⁴ ⊔ x✝³) ⊓ x✝²
⊢ x✝¹ ∈ x✝⁴ ⊔ x✝³ ⊓ x✝²

Tactic:
← sup_inf_assoc_of_le_of_neg_le _ hxy (by simpa)

Goal state after:
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
R✝ : Type u_8
M✝ : Type u_9
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u_10
M : Type u_11
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝⁴ x✝³ x✝² : Submodule R M
hxy : x✝⁴ ≤ x✝²
x✝¹ : M
x✝ : x✝¹ ∈ (x✝⁴ ⊔ x✝³) ⊓ x✝²
⊢ x✝¹ ∈ (x✝⁴ ⊔ x✝³) ⊓ x✝²
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
⊢ ComplementedLattice α ↔ IsAtomistic α

Tactic:
by
  constructor <;> intros
  · exact isAtomistic_of_complementedLattice
  · exact complementedLattice_of_isAtomistic

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
⊢ s.indicator (fun j ↦ f j * g j) i = f i * s.indicator g i

Tactic:
by
  simp only [indicator]
  split_ifs
  · rfl
  · rw [mul_zero]

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

Goal state before:
pp: M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
z : ℤ
x : M
⊢ f ((↑z)⁻¹ • x) = (↑z)⁻¹ • f x

Tactic:
obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg

Goal state after:
case inl
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ f ((↑↑n)⁻¹ • x) = (↑↑n)⁻¹ • f x

case inr
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ f ((↑(-↑n))⁻¹ • x) = (↑(-↑n))⁻¹ • f x
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s : Multiset α
inst✝ : MulLeftMono α
l : List α
hl : ∀ (x : α), x ∈ ⟦l⟧ → 1 ≤ x
⊢ 1 ≤ prod ⟦l⟧

Tactic:
by simpa using List.one_le_prod_of_one_le hl

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f : ι → R
hf0 : ∀ (x : ι), 0 ≤ f x
hf : ∀ (x : ι), f x ≤ 1
x✝¹ x✝ : Finset ι
hst : x✝¹ ⊆ x✝
⊢ ∀ i ∈ x✝, i ∉ x✝¹ → f i ≤ 1

Tactic:
by simp [hf]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: case h₂.h0
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
i : ι
hi : i ∈ s
⊢ i ∈ a :: s

Tactic:
simp [hi]

Goal state after:
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
F : Type u_2
L : Type u_3
inst✝ : FunLike F L R
f : F
r : R
t : Multiset L
hf0 : ∀ (x : L), x ∈ t → 0 ≤ f x
hf : ∀ (x : L), x ∈ t → f x ≤ r
⊢ (map (⇑f) t).prod ≤ r ^ t.card

Tactic:
induction t using Quotient.inductionOn

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulMono R
F : Type u_2
L : Type u_3
inst✝ : FunLike F L R
f : F
r : R
a✝ : List L
hf0 : ∀ (x : L), x ∈ ⟦a✝⟧ → 0 ≤ f x
hf : ∀ (x : L), x ∈ ⟦a✝⟧ → f x ≤ r
⊢ (map ⇑f ⟦a✝⟧).prod ≤ r ^ card ⟦a✝⟧