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

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
x✝ y z : α
xz : x✝ ≤ z
⊢ (x✝ ⊔ y) ⊓ z ≤ x✝ ⊔ y ⊓ z

Tactic:
inf_sup_right,

Goal state after:
α : Type u_1
inst✝ : DistribLattice α
x✝ y z : α
xz : x✝ ≤ z
⊢ x✝ ⊓ z ⊔ y ⊓ z ≤ x✝ ⊔ y ⊓ z
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : OrderBot α
a b : α
⊢ b < a → b = ⊥ ↔ b ≠ ⊥ → b ≤ a → a ≤ b

Tactic:
simp only [Ne, @not_imp_comm (b = ⊥), Classical.not_imp, lt_iff_le_not_ge]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i : IsSimpleOrder αᵒᵈ
⊢ IsSimpleOrder α

Tactic:
· exact
      { exists_pair_ne := @exists_pair_ne αᵒᵈ _
        eq_bot_or_eq_top := fun a => Or.symm (eq_bot_or_eq_top (OrderDual.toDual a)) }

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : SupClosed s
⊢ SupClosed (infClosure s)

Tactic:
rintro _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩

Goal state after:
α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : SupClosed s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ t.inf' ht id ⊔ u.inf' hu id ∈ infClosure s
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
⊢ sSup t ∈ s

Tactic:
have := ht.to_subtype
  have := ht'.to_subtype
  rw [sSup_eq_iSup']
  exact hs.iSup_mem_of_nonempty (by simpa)

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι
x✝² : u ⊆ s
i : ι
x✝¹ : i ∈ s
x✝ : i ∉ u
⊢ Disjoint ((fun i ↦ t.sup fun i' ↦ f (i, i')) i) (u.sup fun i ↦ t.sup fun i' ↦ f (i, i'))

pp: case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι'
x✝² : u ⊆ t
i : ι'
x✝¹ : i ∈ t
x✝ : i ∉ u
⊢ Disjoint ((fun i' ↦ s.sup fun i ↦ f (i, i')) i) (u.sup fun i' ↦ s.sup fun i ↦ f (i, i'))

Tactic:
· suffices Disjoint ((t.image ((i, ·))).sup f) ((u ×ˢ t).sup f) by
      simpa only [sup_image, sup_product_left]
    grind [Finset.SupIndep.disjoint_sup_sup, = product_eq_sprod, = disjoint_left]

Goal state after:
case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι'
x✝² : u ⊆ t
i : ι'
x✝¹ : i ∈ t
x✝ : i ∉ u
⊢ Disjoint ((fun i' ↦ s.sup fun i ↦ f (i, i')) i) (u.sup fun i' ↦ s.sup fun i ↦ f (i, i'))
Module: Mathlib.Algebra.BigOperators.Group.Finset.Lemmas

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → κ → M
⊢ (mulSupport fun x ↦ ∏ i ∈ s, f i x) ⊆ ⋃ i ∈ s, mulSupport (f i)

Tactic:
simp only [mulSupport_subset_iff', Set.mem_iUnion, not_exists, notMem_mulSupport]

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → κ → M
⊢ ∀ (x : κ), (∀ x_1 ∈ s, f x_1 x = 1) → ∏ i ∈ s, f i x = 1
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
⊢ IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k

Tactic:
simp_rw [isCompactElement_iff_exists_le_sSup_of_le_sSup]

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
⊢ IsSupFiniteCompact α ↔ ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
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
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S ↑p
this : map q.subtype (span S (range ⇑(inclusion h₁))) = q
⊢ span S (range ⇑(inclusion h₁)) = ⊤

Tactic:
by
    apply map_injective_of_injective q.injective_subtype
    rw [this, q.map_subtype_top]

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
⊢ (mulSupport f).mulIndicator (f * g) = f

Tactic:
by
  refine (mulIndicator_congr fun x hx => ?_).trans mulIndicator_mulSupport
  have : g x = 1 := notMem_mulSupport.1 (disjoint_left.1 h hx)
  rw [Pi.mul_apply, this, mul_one]

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₂
p : Submodule R M
q : Submodule R₂ M₂
le : comap f q ≤ p
x : M
h : x ∈ comap f (map f p ⊔ q)
y : M
hy : y ∈ ↑p
z : M₂
hz : z ∈ q
eq : z = f x - f y
⊢ x ∈ p

Tactic:
← map_sub

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 τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
le : comap f q ≤ p
x : M
h : x ∈ comap f (map f p ⊔ q)
y : M
hy : y ∈ ↑p
z : M₂
hz : z ∈ q
eq : z = f (x - y)
⊢ x ∈ p
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
b b' : M
hb : b ≠ 0
hb' : b' ≠ 0
i j : α
⊢ Disjoint (single i b).support (single j b').support ↔ i ≠ j

Tactic:
by
  rw [support_single _ hb, support_single _ hb', disjoint_singleton]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
⊢ #f.support = 1 ↔ ∃ a, f a ≠ 0 ∧ f = single a (f a)

Tactic:
simp only [card_eq_one, support_eq_singleton]

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✝² : DecidableEq α
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ (f + g).prod h = f.prod h * g.prod h

Tactic:
by
  rw [Finsupp.prod_of_support_subset f subset_union_left h h_zero,
    Finsupp.prod_of_support_subset g subset_union_right h h_zero, ←
    Finset.prod_mul_distrib, Finsupp.prod_of_support_subset (f + g) Finsupp.support_add h h_zero]
  exact Finset.prod_congr rfl fun x hx => by apply h_add x hx

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
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f ↑s.support
hx_w : α
hx_h_left : ¬s hx_w = 0
⊢ ¬(mapDomain f s) (f hx_w) = 0

Tactic:
rw [mapDomain_apply' (↑s.support : Set _) _ _ hf]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f ↑s.support
hx_w : α
hx_h_left : ¬s hx_w = 0
⊢ ¬s hx_w = 0

α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f ↑s.support
hx_w : α
hx_h_left : ¬s hx_w = 0
⊢ hx_w ∈ ↑s.support

α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f ↑s.support
hx_w : α
hx_h_left : ¬s hx_w = 0
⊢ ↑s.support ⊆ ↑s.support
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg
M : Type u_2
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
f : p → M
h : ¬p
⊢ ∏ᶠ (i : p), f i = 1

Tactic:
have : IsEmpty p := ⟨h⟩

Goal state after:
case neg
M : Type u_2
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
f : p → M
h : ¬p
this : IsEmpty p
⊢ ∏ᶠ (i : p), f i = 1
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg.hnc
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : ¬HasFiniteMulSupport (g ∘ PLift.down)
⊢ ¬HasFiniteMulSupport ((fun i ↦ f (g i)) ∘ PLift.down)

pp: case neg.hnc
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : ¬HasFiniteMulSupport (g ∘ PLift.down)
⊢ ¬HasFiniteMulSupport ((fun i ↦ g i) ∘ PLift.down)

Tactic:
exacts [Infinite.mono (fun x hx => mt (hf (g x.down)) hx) hg, hg]

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

Goal state before:
pp: case pos
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (HasFiniteMulSupport f)
h : HasFiniteMulSupport f
⊢ ∏ᶠ (i : α), f i = ∏ i ∈ Finite.toFinset h, f i

Tactic:
exact finprod_eq_prod_of_mulSupport_toFinset_subset _ h (Finset.Subset.refl _)

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : Basis ι R M
h : f.repr = g.repr
⊢ f = g

Tactic:
cases f

Goal state after:
case ofRepr
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : Basis ι R M
repr✝ : M ≃ₗ[R] ι →₀ R
h : { repr := repr✝ }.repr = g.repr
⊢ { repr := repr✝ } = g
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
i j : ι
inst✝ : Decidable (i = j)
⊢ (b.repr (b i)) j = if i = j then 1 else 0

Tactic:
repr_self,

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
i j : ι
inst✝ : Decidable (i = j)
⊢ (single i 1) j = if i = j then 1 else 0
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
v : α → M
x : M
⊢ x ∈ span R (Set.range v) ↔ ∃ c, (c.sum fun i a ↦ a • v i) = x

Tactic:
simp only [← Finsupp.range_linearCombination, LinearMap.mem_range, linearCombination_apply]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
b : Basis ι R M
x : ι → R
⊢ b.equivFun.symm x = ∑ i, x i • b i

Tactic:
by
  simp [Basis.equivFun, Finsupp.linearCombination_apply, sum_fintype, equivFunOnFinite]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) '' Icc i j = Icc (i.addNat m) (j.addNat m)

Tactic:
← preimage_addNat_Icc_addNat,

Goal state after:
n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) '' (fun x ↦ x.addNat ?m) ⁻¹' Icc (i.addNat ?m) (j.addNat ?m) = Icc (i.addNat m) (j.addNat m)

case m
n m : ℕ
i j : Fin n
⊢ ℕ
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) '' Ioc i j = Ioc (i.addNat m) (j.addNat m)

Tactic:
by
  rw [← preimage_addNat_Ioc_addNat, image_preimage_eq_of_subset]
  exact Ioc_subset_Ioi_self.trans <| image_addNat_Ioi m i ▸ image_subset_range _ _

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ rev ⁻¹' Ioc i j = Ico j.rev i.rev

Tactic:
by
  ext; simp [lt_rev_iff, rev_le_iff, and_comm]

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝¹ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝¹ : Type u_6
M'✝ : Type u_7
M''✝ : Type u_8
V : Type u
V' : Type u_9
inst✝¹⁶ : Semiring R✝¹
inst✝¹⁵ : AddCommMonoid M✝¹
inst✝¹⁴ : Module R✝¹ M✝¹
inst✝¹³ : AddCommMonoid M'✝
inst✝¹² : Module R✝¹ M'✝
ι : Type u_10
R✝ : Type u_11
M✝ : Type u_12
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
b✝ : Basis ι R✝ M✝
inst✝⁸ : Module R✝ M'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι
i' : ι'
hi' : b' i' = f (b i)
⊢ ((b'.constr R) (g ∘ ⇑b') ∘ₗ (b.constr R) (f ∘ ⇑b)) (b i) = LinearMap.id (b i)

Tactic:
LinearMap.comp_apply,

Goal state after:
ι✝ : Type u_1
ι' : Type u_2
R✝¹ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝¹ : Type u_6
M'✝ : Type u_7
M''✝ : Type u_8
V : Type u
V' : Type u_9
inst✝¹⁶ : Semiring R✝¹
inst✝¹⁵ : AddCommMonoid M✝¹
inst✝¹⁴ : Module R✝¹ M✝¹
inst✝¹³ : AddCommMonoid M'✝
inst✝¹² : Module R✝¹ M'✝
ι : Type u_10
R✝ : Type u_11
M✝ : Type u_12
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
b✝ : Basis ι R✝ M✝
inst✝⁸ : Module R✝ M'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι
i' : ι'
hi' : b' i' = f (b i)
⊢ ((b'.constr R) (g ∘ ⇑b')) (((b.constr R) (f ∘ ⇑b)) (b i)) = LinearMap.id (b i)
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝¹ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝¹ : Type u_6
M'✝ : Type u_7
M''✝ : Type u_8
V : Type u
V' : Type u_9
inst✝¹⁶ : Semiring R✝¹
inst✝¹⁵ : AddCommMonoid M✝¹
inst✝¹⁴ : Module R✝¹ M✝¹
inst✝¹³ : AddCommMonoid M'✝
inst✝¹² : Module R✝¹ M'✝
ι : Type u_10
R✝ : Type u_11
M✝ : Type u_12
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
b✝ : Basis ι R✝ M✝
inst✝⁸ : Module R✝ M'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι'
i' : ι
hi' : b i' = g (b' i)
⊢ ((b.constr R) (f ∘ ⇑b) ∘ₗ (b'.constr R) (g ∘ ⇑b')) (b' i) = LinearMap.id (b' i)

Tactic:
LinearMap.comp_apply,

Goal state after:
ι✝ : Type u_1
ι' : Type u_2
R✝¹ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝¹ : Type u_6
M'✝ : Type u_7
M''✝ : Type u_8
V : Type u
V' : Type u_9
inst✝¹⁶ : Semiring R✝¹
inst✝¹⁵ : AddCommMonoid M✝¹
inst✝¹⁴ : Module R✝¹ M✝¹
inst✝¹³ : AddCommMonoid M'✝
inst✝¹² : Module R✝¹ M'✝
ι : Type u_10
R✝ : Type u_11
M✝ : Type u_12
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
b✝ : Basis ι R✝ M✝
inst✝⁸ : Module R✝ M'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι'
i' : ι
hi' : b i' = g (b' i)
⊢ ((b.constr R) (f ∘ ⇑b)) (((b'.constr R) (g ∘ ⇑b')) (b' i)) = LinearMap.id (b' i)
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
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : range ⇑b ⊆ w
x : M
p : x ∈ w
q : x ∉ range ⇑b
e : (linearCombination R ⇑b) (b.repr x) = x
u : ι ↪ ↑w := { toFun := fun i ↦ ⟨b i, ⋯⟩, inj' := ⋯ }
⊢ False

Tactic:
Finsupp.linearCombination_apply

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : range ⇑b ⊆ w
x : M
p : x ∈ w
q : x ∉ range ⇑b
e : ((b.repr x).sum fun i a ↦ a • b i) = x
u : ι ↪ ↑w := { toFun := fun i ↦ ⟨b i, ⋯⟩, inj' := ⋯ }
⊢ False
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inl
y z : ℕ∞
⊢ 1 ^ (y + z) = 1 ^ y * 1 ^ z

pp: case inr.inr
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
· simp only [one_epow, mul_one]

Goal state after:
case inr.inr
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ (y + z) = x ^ y * x ^ z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe
x y z : ℕ∞
a✝ : ℕ
⊢ (x * y) ^ ↑a✝ = x ^ ↑a✝ * y ^ ↑a✝

Tactic:
· simp only [epow_natCast, mul_pow x y]

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

Goal state before:
pp: n a b c : ℕ
⊢ a + n * b ≡ c [MOD n] ↔ a ≡ c [MOD n]

Tactic:
add_modulus_mul_modEq_iff

Goal state after:
n a b c : ℕ
⊢ a ≡ c [MOD n] ↔ a ≡ c [MOD n]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c : ℕ
⊢ n * b + a ≡ c [MOD n] ↔ a ≡ c [MOD n]

Tactic:
by
  rw [add_comm, add_modulus_mul_modEq_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
this✝ : Fintype β
this : Fintype α
⊢ Injective f → (Surjective f ↔ Nat.card α = Nat.card β)

Tactic:
← and_congr_right_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
this✝ : Fintype β
this : Fintype α
⊢ Injective f ∧ Surjective f ↔ Injective f ∧ Nat.card α = Nat.card β
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_3
⊢ card α = 1 ↔ Nonempty (Unique α)

Tactic:
rw [unique_iff_subsingleton_and_nonempty α, le_antisymm_iff]

Goal state after:
α : Type u_3
⊢ card α ≤ 1 ∧ 1 ≤ card α ↔ Subsingleton α ∧ Nonempty α
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
this : Subsingleton M
⊢ ∀ (i : { s // LinearIndepOn R id s }), #↑↑i ≤ 1

Tactic:
simp [Set.subsingleton_of_subsingleton]

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
h : 1 < finrank R M
⊢ 1 < Module.rank R M

Tactic:
by
  simpa using lt_rank_of_lt_finrank h

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a : R
⊢ a % 0 = a

Tactic:
by simpa only [zero_mul, zero_add] using div_add_mod a 0

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

Goal state before:
pp: case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ LinearIndepOn R id (rangeSplitting ⇑f '' s)

Tactic:
apply LinearIndependent.of_comp f.rangeRestrict

Goal state after:
case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ LinearIndependent (ι := ↑(rangeSplitting ⇑f '' s)) R (⇑f.rangeRestrict ∘ fun x ↦ id ↑x)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : t.encard ≤ s.encard
⊢ s = t

Tactic:
rw [← zero_add (a := encard s), ← encard_sdiff_add_encard_of_subset hst] at hts

Goal state after:
α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
⊢ s = t
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
f g : ι → R
⊢ ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i

Tactic:
rw [← sub_eq_zero, ← Finset.sum_sub_distrib]
    convert! h s (f - g) using 3; simp only [Pi.sub_apply, sub_smul, sub_eq_zero]

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

Goal state before:
pp: case succ
α : 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 ⊆ s, t.encard = ↑n + 1

Tactic:
exact ⟨insert x t₀, insert_subset hx.1 ht₀s, by rw [encard_insert_of_notMem hx.2, ht₀]⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hc : t.encard < s.encard
hf : MapsTo f s t
⊢ ∃ a₁ ∈ s, ∃ a₂ ∈ s, a₁ ≠ a₂ ∧ f a₁ = f a₂

Tactic:
contrapose! hc

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
hc : ∀ a₁ ∈ s, ∀ a₂ ∈ s, a₁ ≠ a₂ → f a₁ ≠ f a₂
⊢ s.encard ≤ t.encard
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ x⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s

Tactic:
· intro h z
    rw [← mul_inv_cancel_right x⁻¹ y]
    rw [mul_assoc]
    exact s.mul_mem_cancel_left h

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
⊢ leftRel (s.prod s') = (leftRel s).prod (leftRel s')

Tactic:
by
  refine Setoid.ext fun x y ↦ ?_
  rw [Setoid.prod_apply]
  simp_rw [leftRel_apply]
  rfl

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

Goal state before:
pp: M : Type u_7
R : Type u_8
inst✝⁴ : Ring R
inst✝³ : Nontrivial R
inst✝² : IsAddTorsionFree R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range ⇑b)
i : ι
⊢ ↑((addSubgroupOfClosure A b h) i) = b i

Tactic:
by
  simp [addSubgroupOfClosure]

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
a : ↥s × ↑t
⊢ ↑(Quotient.out ↑a.2 * ↑a.1) ∈ t

Tactic:
rw [mk_mul_of_mem _ a.1.2, out_eq']

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
a : ↥s × ↑t
⊢ ↑a.2 ∈ t
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: case hunique
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∀ (y₁ y₂ : R), x * y₁ = 1 → x * y₂ = 1 → y₁ = y₂

Tactic:
· intro y z hxy hxz
    calc
      y = y * (x * z) := by rw [hxz, mul_one]
      _ = x * y * z := by rw [← mul_assoc, hf.mul_comm y x]
      _ = z := by rw [hxy, one_mul]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' p'' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
⊢ p ≤ comap LinearMap.id p

Tactic:
by rw [comap_id]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
x : M
⊢ (factor H ∘ₗ p.mkQ) x = p'.mkQ x

Tactic:
LinearMap.comp_apply,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
x : M
⊢ (factor H) (p.mkQ x) = p'.mkQ x