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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y, O.subtype y ∈ N ∧ ϕ y = x) → ∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x

pp: case refine_2
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x) → ∃ y, O.subtype y ∈ N ∧ ϕ y = x

Tactic:
· rintro ⟨⟨y, yO⟩, yN : y ∈ N, h⟩
    exact ⟨y, yO, yN, h⟩

Goal state after:
case refine_2
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x) → ∃ y, O.subtype y ∈ N ∧ ϕ y = x
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : Preorder α
⊢ Function.Injective fun c ↦ ⇑c.toOrderHom

Tactic:
rintro ⟨⟩ ⟨⟩ h

Goal state after:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : Preorder α
toOrderHom✝¹ : α →o α
le_closure'✝¹ : ∀ (x : α), x ≤ toOrderHom✝¹.toFun x
idempotent'✝¹ : ∀ (x : α), toOrderHom✝¹.toFun (toOrderHom✝¹.toFun x) = toOrderHom✝¹.toFun x
IsClosed✝¹ : α → Prop
isClosed_iff✝¹ : ∀ {x : α}, IsClosed✝¹ x ↔ toOrderHom✝¹.toFun x = x
toOrderHom✝ : α →o α
le_closure'✝ : ∀ (x : α), x ≤ toOrderHom✝.toFun x
idempotent'✝ : ∀ (x : α), toOrderHom✝.toFun (toOrderHom✝.toFun x) = toOrderHom✝.toFun x
IsClosed✝ : α → Prop
isClosed_iff✝ : ∀ {x : α}, IsClosed✝ x ↔ toOrderHom✝.toFun x = x
h :
  (fun c ↦ ⇑c.toOrderHom)
      { toOrderHom := toOrderHom✝¹, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹, IsClosed := IsClosed✝¹,
        isClosed_iff := isClosed_iff✝¹ } =
    (fun c ↦ ⇑c.toOrderHom)
      { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝, idempotent' := idempotent'✝, IsClosed := IsClosed✝,
        isClosed_iff := isClosed_iff✝ }
⊢ { toOrderHom := toOrderHom✝¹, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹, IsClosed := IsClosed✝¹,
      isClosed_iff := isClosed_iff✝¹ } =
    { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝, idempotent' := idempotent'✝, IsClosed := IsClosed✝,
      isClosed_iff := isClosed_iff✝ }
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝³ : PartialOrder A
inst✝² : SetLike A B
inst✝¹ : IsConcreteLE A B
inst✝ : OrderTop A
K : A
⊢ IsCoatom K ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤

Tactic:
by
  simp_rw [IsCoatom, lt_iff_le_not_ge, SetLike.not_le_iff_exists,
    and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
s : Finset α
⊢ supClosure ↑s ⊆ ↑(Finset.image (fun t ↦ (↑t).sup' ⋯ id) {t ∈ s.powerset | t.Nonempty}.attach)

Tactic:
rintro _ ⟨t, ht, hts, rfl⟩

Goal state after:
α : Type u_3
inst✝ : SemilatticeSup α
s t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ ↑s
⊢ t.sup' ht id ∈ ↑(Finset.image (fun t ↦ (↑t).sup' ⋯ id) {t ∈ s.powerset | t.Nonempty}.attach)
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
⊢ ∃ s_1, IsLUB s_1 s ∧ ∀ a ∈ s_1, IsAtom a

Tactic:
refine ⟨{f | IsAtom f ∧ f ≤ s}, ?_, by simp +contextual⟩

Goal state after:
ι✝ : 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
⊢ IsLUB {f | IsAtom f ∧ f ≤ s} s
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mp
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ range s
ht' : k ≤ t.sup id
f : ↥t → ι
hf : ∀ (x : ↥t), s (f x) = ↑x
⊢ t.sup id ≤ (Finset.image f Finset.univ).sup s

Tactic:
rw [Finset.sup_le_iff]

Goal state after:
case mp
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ range s
ht' : k ≤ t.sup id
f : ↥t → ι
hf : ∀ (x : ↥t), s (f x) = ↑x
⊢ ∀ b ∈ t, id b ≤ (Finset.image f Finset.univ).sup s
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 : Finset ↑s
ht : k ≤ t.sup Subtype.val
⊢ t.sup Subtype.val ≤ (Finset.image Subtype.val t).sup id

Tactic:
rw [Finset.sup_le_iff]

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
⊢ ∀ b ∈ t, ↑b ≤ (Finset.image Subtype.val t).sup id
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
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).toFun ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
rw [algebraMap_apply R S A, algebraMap_apply R S B]
      exact f.commutes (algebraMap R S r)

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
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.toRingEquiv.toFun ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
rw [algebraMap_apply R S A, algebraMap_apply R S B]
      exact f.commutes (algebraMap R S r)

Goal state after:
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
t : Set A
k : S
hks : k ∈ span R s
x : A
hx : x ∈ t
b : R
c : S
x✝ : c ∈ span R s
hc : c • x ∈ span R (s • t)
⊢ (b • c) • x ∈ span R (s • t)

Tactic:
by rw [IsScalarTower.smul_assoc]; exact smul_mem _ _ hc

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : InjOn f {i | f i ≠ ⊥}
⊢ ∀ (i_1 : Finset α), ↑i_1 ⊆ f '' {j | j ≠ i} → Disjoint (f i) (i_1.sup id)

Tactic:
intro s hs

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : InjOn f {i | f i ≠ ⊥}
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
⊢ Disjoint (f i) (s.sup id)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
⊢ ∀ (i_1 : Finset α), ↑i_1 ⊆ f '' {j | j ≠ i} → Disjoint (f i) (i_1.sup id)

Tactic:
intro s hs

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
⊢ Disjoint (f i) (s.sup id)
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'
⊢ p.prod q₁ ⊔ p'.prod q₁' = (p ⊔ p').prod (q₁ ⊔ q₁')

Tactic:
by
  refine le_antisymm
    (sup_le (prod_mono le_sup_left le_sup_left) (prod_mono le_sup_right le_sup_right)) ?_
  simp only [SetLike.le_def, mem_prod, and_imp, Prod.forall]; intro xx yy hxx hyy
  rcases mem_sup.1 hxx with ⟨x, hx, x', hx', rfl⟩
  rcases mem_sup.1 hyy with ⟨y, hy, y', hy', rfl⟩
  exact mem_sup.2 ⟨(x, y), ⟨hx, hy⟩, (x', y'), ⟨hx', hy'⟩, rfl⟩

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

Goal state before:
pp: case add_left
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y : N
u₁ u₂ : M
v : N
hu₁ : u₁ ∈ span R s
hu₂ : u₂ ∈ span R s
hv : v ∈ span R t
huv₁ : (B u₁) v ∈ P'
huv₂ : (B u₂) v ∈ P'
⊢ (B (u₁ + u₂)) v ∈ P'

Tactic:
simpa using add_mem huv₁ huv₂

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

Goal state before:
pp: case add_right
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y : N
u : M
v₁ v₂ : N
hu : u ∈ span R s
hv₁ : v₁ ∈ span R t
hv₂ : v₂ ∈ span R t
huv₁ : (B u) v₁ ∈ P'
huv₂ : (B u) v₂ ∈ P'
⊢ (B u) (v₁ + v₂) ∈ P'

Tactic:
simpa using add_mem huv₁ huv₂

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

Goal state before:
pp: case insert
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
⊢ ∏ a ∈ insert a s, ∑ b ∈ t a, f a b = ∑ p ∈ (insert a s).pi t, ∏ x ∈ (insert a s).attach, f (↑x) (p ↑x ⋯)

Tactic:
have h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y →
      Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t)) := by
      intro x _ y _ h
      simp only [disjoint_iff_ne, mem_image]
      rintro _ ⟨p₂, _, eq₂⟩ _ ⟨p₃, _, eq₃⟩ eq
      have : Pi.cons s a x p₂ a (mem_insert_self _ _)
              = Pi.cons s a y p₃ a (mem_insert_self _ _) := by rw [eq₂, eq₃, eq]
      rw [Pi.cons_same, Pi.cons_same] at this
      exact h this
    rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_biUnion h₁]
    refine sum_congr rfl fun b _ => ?_
    have h₂ : ∀ p₁ ∈ pi s t, ∀ p₂ ∈ pi s t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂ :=
      fun p₁ _ p₂ _ eq => Pi.cons_injective ha eq
    rw [sum_image h₂, mul_sum]
    refine sum_congr rfl fun g _ => ?_
    rw [attach_insert, prod_insert, prod_image]
    · simp only [Pi.cons_same]
      congr with ⟨v, hv⟩
      congr
      exact (Pi.cons_ne (by rintro rfl; exact ha hv)).symm
    · exact fun _ _ _ _ => Subtype.ext ∘ Subtype.mk.inj
    · simpa only [mem_image, mem_attach, Subtype.mk.injEq, true_and,
        Subtype.exists, exists_prop, exists_eq_right] using ha

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

Goal state before:
pp: R : Type u_4
inst✝ : CommRing R
n k : ℕ
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)

Tactic:
rcases le_or_gt k n with hkn | hnk

Goal state after:
case inl
R : Type u_4
inst✝ : CommRing R
n k : ℕ
hkn : k ≤ n
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)

case inr
R : Type u_4
inst✝ : CommRing R
n k : ℕ
hnk : n < k
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ (Multiset.map (single a) (Multiset.map (fun b ↦ f b) s.val)).sum = ∑ b ∈ s, single a (f b)

Tactic:
rw [Multiset.map_map]
    rfl

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

Goal state before:
pp: 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

Tactic:
inv_neg,

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
⊢ ∃ x, 1 < v x

Tactic:
by
  obtain ⟨x, hx₀, hx₁⟩ := h
  rcases hx₁.lt_or_gt with h | h
  · refine ⟨x⁻¹, ?_⟩
    rw [map_inv₀]
    exact (one_lt_inv₀ <| v.pos hx₀).mpr h
  · exact ⟨x, h⟩

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

Goal state before:
pp: case c0
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
⊢ 0 < (map f s).prod

Tactic:
apply prod_pos
      grind

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ f i * ∏ i ∈ s \ {i}, f i

Tactic:
refine le_trans ?_ (mul_le_mul_of_nonneg_right h2i ?_)

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ (g i + h i) * ∏ i ∈ s \ {i}, f i

case refine_2
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ 0 ≤ ∏ i ∈ s \ {i}, f i
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: M : Type u_1
N : Type u_2
ι : Type u_4
inst✝⁴ : CommMonoid N
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
s : Finset ι
b : M
f : ι → N
this : Multiset.map (fun x ↦ b • f x) s.val = Multiset.map (fun x ↦ b • x) (Multiset.map f s.val)
⊢ b ^ s.val.card • (Multiset.map f s.val).prod = b ^ (Multiset.map f s.val).card • (Multiset.map f s.val).prod

Tactic:
Multiset.card_map

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

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
f : End (End R (ι →₀ M)) (ι →₀ M)
g✝ : End R M
m : M
g : (ι →₀ M) →ₗ[R] ι →₀ M := mapRange.linearMap g✝
⊢ (f (single i (g✝ • m))) i = (g (f (single i m))) i

Tactic:
rw [← End.smul_def g, ← map_smul]

Goal state after:
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
f : End (End R (ι →₀ M)) (ι →₀ M)
g✝ : End R M
m : M
g : (ι →₀ M) →ₗ[R] ι →₀ M := mapRange.linearMap g✝
⊢ (f (single i (g✝ • m))) i = (f (g • single i m)) i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
⊢ p (∏ᶠ (i : α), f i)

Tactic:
rw [finprod]

Goal state after:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
⊢ p (if h : HasFiniteMulSupport ((fun i ↦ f i) ∘ PLift.down) then ∏ i ∈ Finite.toFinset h, f i.down else 1)
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ Ioi ↑i ∩ Iio n = Ioo (↑i) n

Tactic:
Ioi_inter_Iio

Goal state after:
n : ℕ
i : Fin n
⊢ Ioo (↑i) n = Ioo (↑i) n
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

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
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ ∑ a ∈ s with f a ≠ 0, f a • g a = ∑ a ∈ s, f a • g a

Tactic:
rw [Finset.sum_filter_of_ne]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ ∀ x ∈ s, f x • g x ≠ 0 → f x ≠ 0
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
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
α' : Type u_7
M' : Type u_8
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
v✝ : α → M
v' : α' → M'
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
r : S
v : α → M
a✝ : α
⊢ (linearCombination R (r • v) ∘ₗ lsingle a✝) 1 = (((RingHom.id S) r • linearCombination R v) ∘ₗ lsingle a✝) 1

Tactic:
simp [smul_comm]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ ∏ᶠ (i : α), f i * g i = (∏ᶠ (i : α), f i) * ∏ᶠ (i : α), g i

Tactic:
classical
    rw [finprod_eq_prod_of_mulSupport_toFinset_subset f hf Finset.subset_union_left,
      finprod_eq_prod_of_mulSupport_toFinset_subset g hg Finset.subset_union_right, ←
      Finset.prod_mul_distrib]
    refine finprod_eq_prod_of_mulSupport_subset _ ?_
    simp only [Finset.coe_union, Finite.coe_toFinset, mulSupport_subset_iff,
      mem_union, mem_mulSupport]
    intro x
    contrapose!
    rintro ⟨hf, hg⟩
    simp [hf, hg]

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

Goal state before:
pp: case hf
α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : α → R
⊢ ∀ x_1 ∈ Finset.univ,
    x_1 ∉ ((linearEquivFunOnFinite R R α).symm x).support →
      (fun i ↦ ⇑((fun i ↦ LinearMap.id.smulRight (v i)) i)) x_1 (((linearEquivFunOnFinite R R α).symm x) x_1) = 0

Tactic:
intro x _ hx
    rw [Finsupp.notMem_support_iff.mp hx]
    exact zero_smul _ _

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

Goal state before:
pp: ι : Type u_10
R : Type u_14
M : Type u_15
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_17
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ ∑ j, (b.repr (b' j)) i * (b'.repr x) j = (b.repr x) i

Tactic:
conv_rhs => rw [← b'.sum_repr x]
  simp_rw [map_sum, map_smul, Finset.sum_apply']
  refine Finset.sum_congr rfl fun j _ => ?_
  rw [Finsupp.smul_apply, smul_eq_mul, mul_comm]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ #(Ioi a) = n - 1 - ↑a

Tactic:
← card_map,

Goal state after:
n : ℕ
a : Fin n
⊢ #(map ?m.20 (Ioi a)) = n - 1 - ↑a

n : ℕ
a : Fin n
⊢ Fin n ↪ ?m.18

n : ℕ
a : Fin n
⊢ Type ?u.17
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case mp
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ k % ↑n < ↑n ∧ ∃ m, a - b = (m * ↑n + k % ↑n) • p

Tactic:
refine ⟨?_, k / n, ?_⟩

Goal state after:
case mp.refine_1
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ k % ↑n < ↑n

case mp.refine_2
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ a - b = (k / ↑n * ↑n + k % ↑n) • p
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
⊢ k / m * (m / n) = k / n

Tactic:
rcases n.eq_zero_or_pos with hn | hn

Goal state after:
case inl
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
hn : n = 0
⊢ k / m * (m / n) = k / n

case inr
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
hn : n > 0
⊢ k / m * (m / n) = k / n
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k / m ∣ c
hnc : k / n ∣ c
hm : m > 0
⊢ k / m.gcd n ∣ c

Tactic:
rcases n.eq_zero_or_pos with hn | hn

Goal state after:
case inr.inl
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k / m ∣ c
hnc : k / n ∣ c
hm : m > 0
hn : n = 0
⊢ k / m.gcd n ∣ c

case inr.inr
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k / m ∣ c
hnc : k / n ∣ c
hm : m > 0
hn : n > 0
⊢ k / m.gcd n ∣ c
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m a b d : ℕ
h : a ≡ b [MOD m]
hdm : d ∣ m
⊢ d ∣ a ↔ d ∣ b

Tactic:
simp only [← modEq_zero_iff_dvd]
  replace h := h.of_dvd hdm
  exact ⟨h.symm.trans, h.trans⟩

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

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hdj : Disjoint s t
h : LinearIndepOn R v (s ∪ t)
⊢ Disjoint (span R (v '' s)) (span R (v '' t))

Tactic:
convert! h.disjoint_span_image (s := (↑) ⁻¹' s) (t := (↑) ⁻¹' t) (hdj.preimage _)

Goal state after:
case e'_4
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hdj : Disjoint s t
h : LinearIndepOn R v (s ∪ t)
⊢ v '' s = (fun x ↦ v ↑x) '' Subtype.val ⁻¹' s

case e'_5
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hdj : Disjoint s t
h : LinearIndepOn R v (s ∪ t)
⊢ v '' t = (fun x ↦ v ↑x) '' Subtype.val ⁻¹' t
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: case h₂
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
w : Cardinal.{v}
hw : w < 1
⊢ ∃ i, w < #↑↑i

Tactic:
exact ⟨⟨{0}, LinearIndepOn.of_subsingleton⟩, hw.trans_eq (Cardinal.mk_singleton _).symm⟩

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ finrank R M = 1

Tactic:
by
  rw [finrank, rank_subsingleton, map_one]

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ (if a0 : 0 = 0 then a
    else
      have x := ⋯;
      gcd (a % 0) 0) =
    a

Tactic:
exact if_pos rfl

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s t r' s' t' : R
⊢ (if _hr : 0 = 0 then (r', s', t')
    else
      have q := r' / 0;
      have x := ⋯;
      xgcdAux (r' % 0) (s' - q * s) (t' - q * t) 0 s t) =
    (r', s', t')

Tactic:
exact if_pos rfl

Goal state after: