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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
n : ℕ
⊢ ((pair a₁ a₂ ha).zip (pair b₁ b₂ hb)) n = (pair (a₁, b₁) (a₂, b₂) ⋯) n

Tactic:
cases n

Goal state after:
case zero
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ ((pair a₁ a₂ ha).zip (pair b₁ b₂ hb)) 0 = (pair (a₁, b₁) (a₂, b₂) ⋯) 0

case succ
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
n✝ : ℕ
⊢ ((pair a₁ a₂ ha).zip (pair b₁ b₂ hb)) (n✝ + 1) = (pair (a₁, b₁) (a₂, b₂) ⋯) (n✝ + 1)
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ a ∈ restrict p o h ↔ p ∧ a ∈ o

Tactic:
by
  dsimp [restrict, mem_eq]; constructor
  · rintro ⟨h₀, h₁⟩
    exact ⟨h₀, ⟨_, h₁⟩⟩
  rintro ⟨h₀, _, h₂⟩; exact ⟨h₀, h₂⟩

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1.inr.inl
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
hsseq : sy ≠ sz
h : sy ⊆ sz
⊢ r y z ∨ r z y

Tactic:
exact (hcs₀ hsz).right (h hysy) hzsz hyz

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

Goal state before:
pp: case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
⊢ ∃ h, Bijective h ∧ ∀ (a : α), R a (h a)

Tactic:
set F : Set α →o Set α :=
    { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ
      monotone' := fun s t hst => by dsimp at hst ⊢; gcongr }

Goal state after:
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
⊢ ∃ h, Bijective h ∧ ∀ (a : α), R a (h a)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
⊢ #↑s ≤ #↑(f ⁻¹' s)

Tactic:
rw [← lift_id #(↑(f ⁻¹' s)), ← lift_id #(↑s)]
  exact mk_preimage_of_subset_range_lift f s h

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

Goal state before:
pp: c : Cardinal.{u}
α : Type u
s : Set α
⊢ (∃ p, #↑p = c) ↔ ∃ p ⊆ s, #↑p = c

Tactic:
← Subtype.exists_set_subtype

Goal state after:
c : Cardinal.{u}
α : Type u
s : Set α
⊢ (∃ p, #↑p = c) ↔ ∃ s_1, #↑(Subtype.val '' s_1) = c
Module: Mathlib.Algebra.GroupWithZero.Action.Basic

Goal state before:
pp: G : Type u_1
G₀ : Type u_2
inst✝² : Group G
inst✝¹ : GroupWithZero G₀
inst✝ : MulDistribMulAction G G₀
g : G
x : G₀
n : ℤ
⊢ g • x ^ n = (g • x) ^ n

Tactic:
cases n

Goal state after:
case ofNat
G : Type u_1
G₀ : Type u_2
inst✝² : Group G
inst✝¹ : GroupWithZero G₀
inst✝ : MulDistribMulAction G G₀
g : G
x : G₀
a✝ : ℕ
⊢ g • x ^ Int.ofNat a✝ = (g • x) ^ Int.ofNat a✝

case negSucc
G : Type u_1
G₀ : Type u_2
inst✝² : Group G
inst✝¹ : GroupWithZero G₀
inst✝ : MulDistribMulAction G G₀
g : G
x : G₀
a✝ : ℕ
⊢ g • x ^ Int.negSucc a✝ = (g • x) ^ Int.negSucc a✝
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst✝⁶ : Semiring R₁
inst✝⁵ : Semiring R₂
inst✝⁴ : Semiring R₃
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
hf : Injective ⇑f
g₁ g₂ : M₁ →ₛₗ[σ₁₂] M₂
h : f ∘ₛₗ g₁ = f ∘ₛₗ g₂
x : M₁
⊢ f (g₁ x) = f (g₂ x)

Tactic:
rw [← comp_apply, h, comp_apply]

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R'
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R' M'
σ₁₂ : R →+* R'
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module S M'
inst✝¹ : SMulCommClass R' S M'
inst✝ : SMulCommClass R S M
x✝¹ : M →ₛₗ[σ₁₂] M'
x✝ : M
⊢ (0 • x✝¹) x✝ = 0 x✝

Tactic:
by
    simp [DomMulAct.smul_linearMap_apply, DomMulAct.mk, MulOpposite.opEquiv]

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : i ∉ s
ih : ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)
⊢ ↑((insert i s).inf p) = ⋂ i_1 ∈ insert i s, ↑(p i_1)

Tactic:
rw [Finset.inf_insert, coe_inf, ih]
    simp

Goal state after:
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : SupSet α
inst✝¹ : SupSet β
inst✝ : SupSet γ
g : sSupHom β γ
f₁ f₂ : sSupHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Goal state after:
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : CompleteLattice γ
g : FrameHom β γ
f₁ f₂ : FrameHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Goal state after:
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : CompleteLattice γ
g : CompleteLatticeHom β γ
f₁ f₂ : CompleteLatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

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

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

Tactic:
by
    induction n with
    | zero => rw [Nat.cast_zero, zero_mul, zero_mul, zero_mul]
    | succ n ihn => rw [Nat.cast_succ, add_mul, one_mul, ihn, add_mul, add_mul, one_mul]

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
g : S →ₙ+* T
f : R →ₙ+* S
⊢ map g (srange f) = srange (g.comp f)

Tactic:
by
  simpa only [srange_eq_map] using! (⊤ : NonUnitalSubsemiring R).map_map g f

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 • z • b y = x • z • (b 1 * b 1)
⊢ (algebraMap F E) (x * y) = b x

Tactic:
rwa [← map_smul, smul_eq_mul, mul_comm, ← smul_mul_assoc, ← map_smul _ z, smul_eq_mul, mul_one,
    ← smul_eq_mul, map_smul, hz, one_mul, ← map_smul, smul_eq_mul, mul_one, smul_smul,
    ← Algebra.algebraMap_eq_smul_one] at hy

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p x y : M
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
⊢ p ^ (i + 1) ∣ x ∨ p ∣ y

Tactic:
by
  rw [or_iff_not_imp_right]
  exact fun a ↦ Prime.pow_dvd_of_dvd_mul_right h (i + 1) a hxy

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

Goal state before:
pp: case succ.inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p * p ^ n
hno : q ∣ p ^ n
⊢ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i

Tactic:
obtain ⟨i, hi, hq⟩ := ih.mp hno
      exact ⟨i, hi.trans n.le_succ, hq⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] M
n : ℕ
⊢ f.iterateRange (n + 1) = map f (f.iterateRange n)

Tactic:
simp only [iterateRange_coe, range_eq_map, ← map_comp, Module.End.iterate_succ']

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

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₂
module_M : Module R M
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
p : Submodule R M
inst✝ : Module R₂ M₂
e : ↥p ≃ₛₗ[σ₁₂] ↥⊥
⊢ p = ⊥

Tactic:
by
  refine bot_unique (SetLike.le_def.2 fun b hb => (Submodule.mem_bot R).2 ?_)
  rw [← p.mk_eq_zero hb, ← e.map_eq_zero_iff]
  apply Submodule.eq_zero_of_bot_submodule

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
h : p ≤ q
⊢ (inclusion h).range = comap q.subtype p

Tactic:
by
  rw [← map_top, inclusion, LinearMap.map_codRestrict, map_top, range_subtype]

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

Goal state before:
pp: case smul.add
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
r₁ : R
y x✝ y✝ : M
hx✝ : x✝ ∈ closure (univ • s)
hy✝ : y✝ ∈ closure (univ • s)
h₁ : r₁ • x✝ ∈ closure (univ • s)
h₂ : r₁ • y✝ ∈ closure (univ • s)
⊢ r₁ • (x✝ + y✝) ∈ closure (univ • s)

Tactic:
simpa only [smul_add] using add_mem h₁ h₂

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
a b : α
⊢ a = b ↔ ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)

Tactic:
refine ⟨fun h => by simp [h], fun h => ?_⟩

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
⊢ a = b
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_1.inr
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
k : ι
hjk : j ≠ k
⊢ update v j (v j + r • v i) k ∈ span R (range v)

pp: case refine_2.inl
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
⊢ v j ∈ span R (range (update v j (v j + r • v i)))

pp: case refine_2.inr
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
k : ι
hjk : j ≠ k
⊢ v k ∈ span R (range (update v j (v j + r • v i)))

Tactic:
· exact subset_span ⟨k, (update_of_ne hjk.symm ..).symm⟩

Goal state after:
case refine_2.inl
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
⊢ v j ∈ span R (range (update v j (v j + r • v i)))

case refine_2.inr
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
k : ι
hjk : j ≠ k
⊢ v k ∈ span R (range (update v j (v j + r • v i)))
Module: Mathlib.Order.Interval.Set.OrderIso

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

Tactic:
ext x
  simp [← e.le_iff_le]

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

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : M
ha : p = R ∙ a
x : ↥p
x✝ : x ∈ ⊤
⊢ x ∈ R ∙ ⟨a, ⋯⟩

Tactic:
have ⟨r, hr⟩ := mem_span_singleton.mp (ha.le x.2)

Goal state after:
case mpr
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : M
ha : p = R ∙ a
x : ↥p
x✝ : x ∈ ⊤
r : R
hr : r • a = ↑x
⊢ x ∈ R ∙ ⟨a, ⋯⟩
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: 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
k : S
x : A
hx : x ∈ restrictScalars R (span S t)
⊢ k • x ∈ restrictScalars R (span S t)

Tactic:
exact (span S t).smul_mem k hx

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

Goal state before:
pp: R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
⊢ Injective ⇑(inclusionSpan S p)

Tactic:
intro x y hxy
  rw [Subtype.ext_iff] at hxy
  simpa using hxy

Goal state after:
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
⊢ ∏ i ∈ s, (f i).indicator (g i) j = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) j

Tactic:
rw [Set.indicator]

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
⊢ ∏ i ∈ s, (f i).indicator (g i) j = if j ∈ ⋂ x ∈ s, f x then (∏ i ∈ s, g i) j else 0
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
⊢ Disjoint (⨆ i ∈ s, f i) a

Tactic:
simp_rw [disjoint_iff, iSup_subtype', ← sSup_range, inf_comm, inf_sSup_eq_iSup_inf_sup_finset,
    iSup_eq_bot]
  intro u hu
  obtain ⟨t, ht, ht', htu⟩ : ∃ᵉ (t ⊆ s) (hu : t.Finite), f '' t = u :=
    Set.Finite.exists_subset_finite_image_eq u.finite_toSet <| by rwa [Set.image_eq_range f s]
  replace htu : u.sup id = ⨆ i ∈ t, f i := by
    simp only [Finset.sup_eq_iSup, id_eq, ← Finset.mem_coe, ← htu, iSup_image]
  rw [inf_comm, ← disjoint_iff, htu]
  exact hs t ht ht'

Goal state after:
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:
by
  classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s his h => simp [his, h]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
ι : Sort u_8
p : ι → Submodule R M
h : f.ker ≤ ⨅ i, p i
⊢ map f (⨅ i, p i) = ⨅ i, map f (p i)

Tactic:
conv_rhs => rw [← map_comap_eq_of_surjective hf (⨅ _, _), comap_iInf]
  simp_rw [fun i ↦ comap_map_eq_self (le_iInf_iff.mp h i)]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
ι : Type u_8
s : Set ι
p : ι → Submodule R₂ M₂
hp : ⨆ x, p ↑x = ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
k : ι
hk : k ∈ s
⊢ (⨆ x, comap f (p ↑x)) ⊔ f.ker = ⊤

Tactic:
← comap_map_eq,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
ι : Type u_8
s : Set ι
p : ι → Submodule R₂ M₂
hp : ⨆ x, p ↑x = ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
k : ι
hk : k ∈ s
⊢ comap f (map f (⨆ x, comap f (p ↑x))) = ⊤
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f : ι → R
⊢ ∏ i ∈ s, (1 - f i) = 1 - ∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 - f j)

Tactic:
rw [prod_sub_ordered]

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f : ι → R
⊢ ∏ i ∈ s, 1 - ∑ i ∈ s, (f i * ∏ j ∈ s with j < i, (1 - f j)) * ∏ j ∈ s with i < j, 1 =
    1 - ∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 - f j)
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: case inr
ι : Type u_5
s✝ : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s✝, n ∣ f i
hn : n ≠ 0
s : ι
hs : s ∈ s✝
⊢ f s = f s / n * n

Tactic:
Int.ediv_mul_cancel (hf _ hs)

Goal state after:
case inr
ι : Type u_5
s✝ : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s✝, n ∣ f i
hn : n ≠ 0
s : ι
hs : s ∈ s✝
⊢ f s = f s
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:
by
  classical exact Pi.single_eq_of_ne h _

Goal state after:
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s : Finset ι
f : ι →₀ M
h : f.support = ∅
⊢ motive f

pp: case refine_2
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
⊢ motive f

Tactic:
· rwa [support_eq_empty.1 h]

Goal state after:
case refine_2
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
⊢ motive f
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
⊢ (⋃ i, s i).mulIndicator f x = ⨆ i, (s i).mulIndicator f x

Tactic:
by
  by_cases hx : x ∈ ⋃ i, s i
  · rw [mulIndicator_of_mem hx]
    rw [mem_iUnion] at hx
    refine le_antisymm ?_ (iSup_le fun i ↦ mulIndicator_le_self' (fun x _ ↦ h1 ▸ bot_le) x)
    rcases hx with ⟨i, hi⟩
    exact le_iSup_of_le i (ge_of_eq <| mulIndicator_of_mem hi _)
  · rw [mulIndicator_of_notMem hx]
    simp only [mem_iUnion, not_exists] at hx
    simp [hx, ← h1]

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

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
⊢ g y (f y) * (erase y f).prod g = f.prod g

Tactic:
by_cases hyf : y ∈ f.support

Goal state after:
case pos
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : y ∈ f.support
⊢ g y (f y) * (erase y f).prod g = f.prod g

case neg
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : y ∉ f.support
⊢ g y (f y) * (erase y f).prod g = f.prod g
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ max (List.map f l).prod (List.map g l).prod ≤ (List.map (fun i ↦ max (f i) (g i)) l).prod

Tactic:
apply List.max_prod_le

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
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S

Tactic:
· apply Set.union_subset hv₁ hv₂
          exact mod_cast h

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

Goal state before:
pp: ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
⊢ l.support = l.splitSupport.sigma fun i ↦ (l.split i).support

Tactic:
simp_rw [Finset.ext_iff, splitSupport, split, comapDomain, Sigma.forall, mem_sigma, mem_image,
    mem_preimage]

Goal state after:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
⊢ ∀ (a : ι) (b : αs a), ⟨a, b⟩ ∈ l.support ↔ (∃ a_1 ∈ l.support, a_1.fst = a) ∧ ⟨a, b⟩ ∈ l.support
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
αs : ι → Type u_12
inst✝² : Zero M
l : (i : ι) × αs i →₀ M
η : Type u_13
inst✝¹ : Fintype η
ιs : η → Type u_14
inst✝ : Zero α
f : (j : η) × ιs j →₀ α
⊢ (fun f ↦ onFinset (univ.sigma fun j ↦ (f j).support) (fun ji ↦ (f ji.fst) ji.snd) ⋯) f.split = f

Tactic:
by
    ext
    simp [split]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
αs : ι → Type u_12
inst✝² : Zero M
l : (i : ι) × αs i →₀ M
η : Type u_13
inst✝¹ : Fintype η
ιs : η → Type u_14
inst✝ : Zero α
f : (j : η) → ιs j →₀ α
⊢ ((fun f ↦ onFinset (univ.sigma fun j ↦ (f j).support) (fun ji ↦ (f ji.fst) ji.snd) ⋯) f).split = f

Tactic:
by
    ext
    simp [split]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : Semiring S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R₂ N
inst✝³ : AddCommMonoid P
inst✝² : Module R₃ P
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
α' : Type u_9
α'' : Type u_10
f : α ≃ α'
x✝ : α →₀ M
⊢ mapDomain (⇑f.symm) ((lmapDomain M R f.toFun).toFun x✝) = x✝

Tactic:
by
    simp [← mapDomain_comp]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : Semiring S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R₂ N
inst✝³ : AddCommMonoid P
inst✝² : Module R₃ P
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
α' : Type u_9
α'' : Type u_10
f : α ≃ α'
x✝ : α' →₀ M
⊢ (lmapDomain M R f.toFun).toFun (mapDomain (⇑f.symm) x✝) = x✝

Tactic:
by
    simp [← mapDomain_comp]

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

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝² : Semiring R
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v' : α' → M'
f : α ↪ α'
l : α →₀ R
⊢ (linearCombination R v') (embDomain f l) = (linearCombination R (v' ∘ ⇑f)) l

Tactic:
simp [linearCombination_apply, Finsupp.sum, support_embDomain, embDomain_apply]

Goal state after: