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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
a : α
⊢ Ioi a = {⊤} ↔ IsCoatom a

Tactic:
simp [IsCoatom, superset_antisymm_iff, lt_top_iff_ne_top]

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
h : SupClosed s
ha : a ∈ lowerBounds s
⊢ SupClosed (insert a s)

Tactic:
rw [SupClosed]
  have ha' : ∀ b ∈ s, a ≤ b := fun _ a ↦ ha a
  aesop

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
⊢ p a has

Tactic:
have h : IsSublattice { a : α | ∃ has : a ∈ latticeClosure s, p a has } := {
    supClosed := fun a ⟨has, hpa⟩ b ⟨hbs, hpb⟩ =>
      ⟨isSublattice_latticeClosure.supClosed has hbs, sup a has b hbs hpa hpb⟩
    infClosed := fun a ⟨has, hpa⟩ b ⟨hbs, hpb⟩ =>
      ⟨isSublattice_latticeClosure.infClosed has hbs, inf a has b hbs hpa hpb⟩ }
  refine (latticeClosure_min (fun a ha ↦ ?_) h has).choose_spec
  exact ⟨subset_latticeClosure ha, mem a ha⟩

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

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

Tactic:
span_range_update_add_smul hij

Goal state after:
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ span R (range v) = span R (range v)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
M₂ : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
f : M →ₗ[R] M₂
hf : Function.Surjective ⇑f
inst✝ : IsPrincipal R M
m : M
hm : ⊤ = R ∙ m
⊢ ∃ a, ⊤ = R ∙ a

Tactic:
refine ⟨f m, .symm <| top_unique fun y _ ↦ ?_⟩

Goal state after:
R : Type u_1
M : Type u_4
M₂ : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
f : M →ₗ[R] M₂
hf : Function.Surjective ⇑f
inst✝ : IsPrincipal R M
m : M
hm : ⊤ = R ∙ m
y : M₂
x✝ : y ∈ ⊤
⊢ y ∈ R ∙ f m
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 : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
j : π i
hj : j ∈ upperBounds (Function.eval i '' {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s})
x : π i
x✝ : x ∈ {a | IsAtom a ∧ a ≤ s i}
hx₁ : IsAtom x
hx₂ : x ≤ s i
⊢ Function.update ⊥ i x ≤ s

Tactic:
simp [update_le_iff, hx₂]

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

Goal state before:
pp: case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ IsCompactElement k → ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x

pp: case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ (∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x) → IsCompactElement k

Tactic:
· intro hk s hs hs' h_le
    exact hk s (sSup s) hs hs' (isLUB_sSup s) h_le

Goal state after:
case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ (∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x) → IsCompactElement k
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
⊢ s.mulIndicator f = f ↔ mulSupport f ⊆ s

Tactic:
by
  simp only [funext_iff, subset_def, mem_mulSupport, mulIndicator_apply_eq_self, not_imp_comm]

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

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
⊢ s.mulIndicator f x = s.mulIndicator g x

Tactic:
simp only [mulIndicator]
    split_ifs with h_1
    · exact h h_1
    rfl

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
r : R
⊢ f ((algebraMap S A) ((algebraMap R S) r)) = (algebraMap R B) r

Tactic:
f.commutes,

Goal state after:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
r : R
⊢ (algebraMap S B) ((algebraMap R S) r) = (algebraMap R B) r
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case inr
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a | IsAtom a ∧ a ≤ b} < b
c : { x // x ∈ Iic b }
hc : IsCompl ⟨sSup {a | IsAtom a ∧ a ≤ b}, hle⟩ c
a : { x // x ∈ Iic b }
ha : IsAtom a
hac : a ≤ c
⊢ a = ⊥

Tactic:
rw [eq_bot_iff]

Goal state after:
case inr
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a | IsAtom a ∧ a ≤ b} < b
c : { x // x ∈ Iic b }
hc : IsCompl ⟨sSup {a | IsAtom a ∧ a ≤ b}, hle⟩ c
a : { x // x ∈ Iic b }
ha : IsAtom a
hac : a ≤ c
⊢ a ≤ ⊥
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
hyzx : z = -y + x
⊢ z ∈ p

Tactic:
simpa [hyzx] using p.add_mem (neg_le.mp hnsp hy) hx

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

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

Tactic:
exact complementedLattice_of_isAtomistic

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_4
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : β
h : a ∉ Set.range ⇑f
⊢ (embDomain f v) a = 0

Tactic:
grind [embDomain]

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
a b : R
s : Finset ι
⊢ ∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t) = ∏ _x ∈ s, (a + b)

Tactic:
prod_add

Goal state after:
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
a b : R
s : Finset ι
⊢ ∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t) = ∑ t ∈ s.powerset, (∏ i ∈ t, a) * ∏ i ∈ s \ t, b
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
h : a' ≠ a
⊢ (single a b) a' = 0

Tactic:
classical exact Pi.single_eq_of_ne h _

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

Goal state before:
pp: case refine_2
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1
h₁ : f a = 0 → g a 0 = 1
h : f a = 0
⊢ g a 0 = 1

Tactic:
exact h₁ h

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

Goal state before:
pp: case refine_1
α : Type u_1
d : α →₀ ℕ
h1 : (d.sum fun x n ↦ n) = 1
hd0 : d ≠ 0
⊢ ∃ a, d = single a 1

Tactic:
obtain ⟨a, ha⟩ := ne_iff.mp hd0

Goal state after:
case refine_1
α : Type u_1
d : α →₀ ℕ
h1 : (d.sum fun x n ↦ n) = 1
hd0 : d ≠ 0
a : α
ha : d a ≠ 0 a
⊢ ∃ a, d = single a 1
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inr.inr
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ (if x + y = 0 then 0 else 1) ≤ 2

Tactic:
rcases eq_or_ne (x + y) 0 with hxy | hxy <;> simp [hxy, one_le_two]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case h
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
l : List α
hps : ∀ (a : α), a ∈ ⟦l⟧ → p a
⊢ f (prod ⟦l⟧) ≤ (map f ⟦l⟧).prod

Tactic:
| h l =>

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case h
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
⊢ f (prod ⟦l⟧) ≤ (map f ⟦l⟧).prod

Tactic:
| h l =>

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case h
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
l : List α
hs_nonempty : ⟦l⟧ ≠ ∅
hs : ∀ (a : α), a ∈ ⟦l⟧ → p a
⊢ f (prod ⟦l⟧) ≤ (map f ⟦l⟧).prod

Tactic:
| h l =>

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
s : Multiset α
hs_nonempty : s ≠ ∅
hs : ∀ (a : α), a ∈ s → p a
⊢ f s.prod ≤ (map f s).prod

Tactic:
by
  induction s using Quotient.inductionOn with
  | h l =>
    simp [l.le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul
      (by simpa using hs_nonempty) (by simpa)]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case h
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
hs_nonempty : ⟦l⟧ ≠ ∅
⊢ f (prod ⟦l⟧) ≤ (map f ⟦l⟧).prod

Tactic:
| h l =>

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case mk
ι : Type u_1
α : Type u_2
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : IsOrderedCancelMonoid α
inst✝ : MulLeftStrictMono α
s : Multiset ι
f g : ι → α
l : List ι
hle : ∀ (i : ι), i ∈ Quot.mk (⇑(List.isSetoid ι)) l → f i ≤ g i
hlt : ∃ i, i ∈ Quot.mk (⇑(List.isSetoid ι)) l ∧ f i < g i
⊢ (List.map f l).prod < (List.map g l).prod

Tactic:
exact List.prod_lt_prod' f g hle hlt

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case h
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
m : Multiset α
f : α → β
h_one : f 1 ≤ 0
h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b
l : List α
⊢ f (prod ⟦l⟧) ≤ (map f ⟦l⟧).sum

Tactic:
| h l =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
x : α →₀ M
a : β
h : a ∉ Set.range f
⊢ a ∉ f '' ↑x.support

Tactic:
Set.image_subset_range

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
x : α →₀ M
a : β
h : a ∉ Set.range f
⊢ a ∉ Set.range f
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝³ : CommMonoid N
inst✝² : Preorder N
s : Finset ι
ι' : Type u_9
inst✝¹ : DecidableEq ι'
inst✝ : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
⊢ f a ≤ f a ^ #({a_1 ∈ s | g a_1 = a})

Tactic:
obtain ⟨i, hi, hig⟩ := Finset.mem_image.mp hag

Goal state after:
ι : Type u_1
N : Type u_5
inst✝³ : CommMonoid N
inst✝² : Preorder N
s : Finset ι
ι' : Type u_9
inst✝¹ : DecidableEq ι'
inst✝ : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
i : ι
hi : i ∈ s
hig : g i = a
⊢ f a ≤ f a ^ #({a_1 ∈ s | g a_1 = a})
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: ι₁ : Type u_12
ι₂ : Type u_13
α : Type u_14
M : Type u_15
inst✝¹ : Zero α
inst✝ : CommMonoid M
f₁ : ι₁ →₀ α
f₂ : ι₂ →₀ α
g : ι₁ ⊕ ι₂ → α → M
⊢ (f₁.sumElim f₂).prod g = f₁.prod (g ∘ Sum.inl) * f₂.prod (g ∘ Sum.inr)

Tactic:
simp [Finsupp.prod, Finset.prod_disjSum]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝² : Monoid G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g g' : G
f : α →₀ M
⊢ (g * g') • f = g • g' • f

Tactic:
by
    rw [comapSMul_def, comapSMul_def, comapSMul_def, ← comp_smul_left, mapDomain_comp]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : Codisjoint (supported M R s) (supported M R t)
a : α
⊢ a ∈ ⊤ → a ∈ s ⊔ t

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : M)

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : Codisjoint (supported M R s) (supported M R t)
a : α
x : M
hx : x ≠ 0
⊢ a ∈ ⊤ → a ∈ s ⊔ t
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
this : (mulSupport fun x ↦ (fun x ↦ 1) x.down) ⊆ ↑∅
⊢ ∏ᶠ (x : α), 1 = 1

Tactic:
finprod_eq_prod_plift_of_mulSupport_subset this,

Goal state after:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
this : (mulSupport fun x ↦ (fun x ↦ 1) x.down) ⊆ ↑∅
⊢ ∏ i ∈ ∅, 1 = 1
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
this : mulSupport (f ∘ PLift.down) ⊆ ↑{{ down := a }}
⊢ ∏ᶠ (x : α), f x = f a

Tactic:
finprod_eq_prod_plift_of_mulSupport_subset this,

Goal state after:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
this : mulSupport (f ∘ PLift.down) ⊆ ↑{{ down := a }}
⊢ ∏ i ∈ {{ down := a }}, f i.down = f a
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype ↑I
⊢ ∏ᶠ (i : ↑I) (a : α) (_ : a ∈ t ↑i), f a = ∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j

pp: case h
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype ↑I
⊢ Pairwise (Disjoint on fun x ↦ t ↑x)

pp: case ht
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype ↑I
⊢ ∀ (i : ↑I), (t ↑i).Finite

Tactic:
← finprod_set_coe_eq_finprod_mem

Goal state after:
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype ↑I
⊢ ∏ᶠ (i : ↑I) (a : α) (_ : a ∈ t ↑i), f a = ∏ᶠ (j : ↑I) (j_1 : α) (_ : j_1 ∈ t ↑j), f j_1

case h
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype ↑I
⊢ Pairwise (Disjoint on fun x ↦ t ↑x)

case ht
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype ↑I
⊢ ∀ (i : ↑I), (t ↑i).Finite
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r

Tactic:
by_cases hr : r = 0
  · simp_all
  by_cases h : f.support.Finite
  · exact finsum_mul' f r h
  simp [finsum_def, HasFiniteSupport, h, (by aesop : (f · * r).support = f.support)]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
s : Set ι
l : ι →₀ R
hl : l ∈ supported R R s
hm : (linearCombination R ⇑b) l ∈ span R (⇑b '' s)
⊢ ↑(b.repr ((linearCombination R ⇑b) l)).support ⊆ s

Tactic:
repr_linearCombination,

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
s : Set ι
l : ι →₀ R
hl : l ∈ supported R R s
hm : (linearCombination R ⇑b) l ∈ span R (⇑b '' s)
⊢ ↑l.support ⊆ s
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
⊢ x = 1

Tactic:
have := epow_right_mono x_2.ne_zero (Order.one_le_iff_ne_zero.2 y_0)
    simp only [epow_one, h] at this
    exact (not_lt_of_ge this x_2).rec

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : MulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
w : ι → G
⊢ LinearIndependent R (w • v) ↔ LinearIndependent R v

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.group_smul w⟩

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : MulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
w : ι → G
h : LinearIndependent R (w • v)
⊢ LinearIndependent R v
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
inst✝² : Semiring R
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
⊢ i = j

Tactic:
have h_single_eq : Finsupp.single i c = Finsupp.single j d :=
    li <| by simpa [Finsupp.linearCombination_apply] using h
  rcases (Finsupp.single_eq_single_iff ..).mp h_single_eq with (⟨H, _⟩ | ⟨hc, _⟩)
  · exact H
  · contradiction

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case right.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑m ∣ ↑b - (↑b - ↑m * n.gcdB m * ((↑b - ↑a) / ↑(n.gcd m)))

pp: case right.refine_1.hcb
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑(n.gcd m) ∣ ↑m * n.gcdB m * (↑b - ↑a)

Tactic:
← sub_add,

Goal state after:
case right.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑m ∣ ↑b - ↑b + ↑m * n.gcdB m * ((↑b - ↑a) / ↑(n.gcd m))

case right.refine_1.hcb
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑(n.gcd m) ∣ ↑m * n.gcdB m * (↑b - ↑a)
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: n : ℕ
x✝² x✝¹ x✝ : Fin n
a : ℕ
isLt✝² : a < n
b : ℕ
isLt✝¹ : b < n
c : ℕ
isLt✝ : c < n
⊢ a * (b + c) ≡ a * b + a * c [MOD n]

Tactic:
rw [mul_add]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
inst✝ : IsEmpty α
⊢ Nat.card α = 0

Tactic:
simp [Nat.card]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: R₀ : Type u_1
S₀ : Type u_2
inst✝⁵ : CommSemiring R₀
inst✝⁴ : Semiring S₀
inst✝³ : Algebra R₀ S₀
R₁ : Type u_3
S₁ : Type u_4
inst✝² : CommSemiring R₁
inst✝¹ : Semiring S₁
inst✝ : Algebra R₁ S₁
i : R₀ ≃+* R₁
j : S₀ ≃+* S₁
hc : (algebraMap R₁ S₁).comp i.toRingHom = j.toRingHom.comp (algebraMap R₀ S₀)
⊢ finrank R₀ S₀ = finrank R₁ S₁

Tactic:
by
  simpa using! (congr_arg Cardinal.toNat (lift_rank_eq_of_equiv_equiv i j hc))

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ ↑k
⊢ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k

Tactic:
rwa [ENat.le_natCast_iff] at h

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
hs : s.Finite
⊢ (t \ s).encard = t.encard - s.encard

Tactic:
rw [← @Set.encard_sdiff_add_encard_of_subset _ s t h]

Goal state after:
α : Type u_1
s t : Set α
h : s ⊆ t
hs : s.Finite
⊢ (t \ s).encard = (t \ s).encard + s.encard - s.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = ↑n
hk : ↑n + 1 ≤ s.encard
hne : t₀ ≠ s
x : α
hx : x ∈ s ∧ x ∉ t₀
⊢ t₀.encard + 1 = ↑n + 1

Tactic:
ht₀

Goal state after:
α : Type u_1
s : Set α
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = ↑n
hk : ↑n + 1 ≤ s.encard
hne : t₀ ≠ s
x : α
hx : x ∈ s ∧ x ∉ t₀
⊢ ↑n + 1 = ↑n + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
hf : Function.Injective f
ht : t ⊆ range f
⊢ (f ⁻¹' t).encard = t.encard

Tactic:
rw [← hf.encard_image, image_preimage_eq_inter_range, inter_eq_self_of_subset_left ht]

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

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s : Set ι
⊢ (∀ (i : ↑s), v ↑i ∉ span K (v ∘ Subtype.val '' (univ \ {i}))) ↔ ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))

Tactic:
Set.image_comp

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s : Set ι
⊢ (∀ (i : ↑s), v ↑i ∉ span K (v '' Subtype.val '' (univ \ {i}))) ↔ ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
⊢ α ≃ Fin (Nat.card α)

Tactic:
have := (Finite.exists_equiv_fin α).choose_spec.some

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
this : α ≃ Fin ⋯.choose
⊢ α ≃ Fin (Nat.card α)