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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
h : g ∘ₛₗ f = 0
x : M₂
hx : x ∈ f.range
y : M
hy : f y = x
⊢ g (f y) = 0

Tactic:
← comp_apply,

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
h : g ∘ₛₗ f = 0
x : M₂
hx : x ∈ f.range
y : M
hy : f y = x
⊢ (g ∘ₛₗ f) y = 0
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:
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.Equiv

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
⊢ ↥(map p.subtype q) → ↥q

Tactic:
rintro ⟨x, hx⟩
      refine ⟨⟨x, ?_⟩, ?_⟩ <;> rcases hx with ⟨⟨_, h⟩, _, rfl⟩ <;> assumption

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ r • s ⊆ ↑(span R s)

Tactic:
rintro _ ⟨x, hx, rfl⟩

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
x : M
hx : x ∈ s
⊢ (fun x ↦ r • x) x ∈ ↑(span R s)
Module: Mathlib.Order.SupClosed

Goal state before:
pp: ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ ↑(t ∪ u) ⊆ s

Tactic:
rw [coe_union]

Goal state after:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ ↑t ∪ ↑u ⊆ s
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ SupSet.sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
h : ¬SupSet.sSup s < k
sSup' : SupSet.sSup s ≤ k
sSup : SupSet.sSup s = k
⊢ False

Tactic:
obtain ⟨x, hxs, hkx⟩ := hk s hemp hdir sSup.symm.le

Goal state after:
α : Type u_3
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ SupSet.sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
h : ¬SupSet.sSup s < k
sSup' : SupSet.sSup s ≤ k
sSup : SupSet.sSup s = k
x : α
hxs : x ∈ s
hkx : k ≤ x
⊢ False
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝¹ : One M
s : Set α
f : α → M
a : α
inst✝ : Decidable (a ∈ s)
⊢ s.mulIndicator f a = if a ∈ s then f a else 1

Tactic:
unfold mulIndicator

Goal state after:
α : Type u_1
M : Type u_3
inst✝¹ : One M
s : Set α
f : α → M
a : α
inst✝ : Decidable (a ∈ s)
⊢ (if a ∈ s then f a else 1) = if a ∈ s then f a else 1
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 : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t
⊢ Disjoint (f i) ((Finset.image f ((insert i (t.preimage f hf)).erase i)).sup id)

Tactic:
Finset.sup_image

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t
⊢ Disjoint (f i) (((insert i (t.preimage f hf)).erase i).sup (id ∘ f))
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ ψ : ((i : ι) → M i) →* M'
⊢ (fun i ↦ (φ * ψ).comp (MonoidHom.mulSingle M i)) =
    (fun i ↦ φ.comp (MonoidHom.mulSingle M i)) * fun i ↦ ψ.comp (MonoidHom.mulSingle M i)

Tactic:
by
    ext
    simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.mulSingle_apply,
      MonoidHom.mul_apply, mul_apply]

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ a ∈ s.pi fun x ↦ {True, False}, ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) = a x x_1

Tactic:
eq_iff_iff,

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ a ∈ s.pi fun x ↦ {True, False}, ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1
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 : ⨆ i ∈ s, p i = ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
k : ι
hk : k ∈ s
this : (⨆ i ∈ s, comap f (p i)) ⊔ f.ker = ⊤
⊢ ⨆ i ∈ s, comap f (p i) = ⊤

Tactic:
by
    rw [← this, left_eq_sup]; exact le_trans f.ker_le_comap (le_biSup (fun i ↦ (p i).comap f) hk)

Goal state after:
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: α : Type u_1
p₁ p₂ : α → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
s : Multiset α
hp₁ : {x | x ∈ s ∧ p₁ x}.Subsingleton
h : ∀ (x : α), x ∈ s → (p₁ x ↔ p₂ x)
⊢ find? p₁ s hp₁ = find? p₂ s ⋯

Tactic:
by
  induction s using Quotient.ind
  exact List.find?_congr fun x hx ↦ by simp [h x (by simpa using hx)]

Goal state after:
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
⊢ ∑ i ∈ s, f i = (∑ i ∈ s, f i / n) * n

Tactic:
sum_mul

Goal state after:
case inr
ι : Type u_5
s : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s, n ∣ f i
hn : n > 0
⊢ ∑ i ∈ s, f i = ∑ i ∈ s, f i / n * n
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
⊢ ∑ i ∈ s, f i = (∑ i ∈ s, f i / n) * n

Tactic:
sum_mul

Goal state after:
case inr
ι : Type u_5
s : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s, n ∣ f i
hn : n ≠ 0
⊢ ∑ i ∈ s, f i = ∑ i ∈ s, f i / n * n
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
s : Finset α
f : α → β →₀ M
⊢ (s.sum f).support ⊆ s.sup fun x ↦ (f x).support

Tactic:
induction s using Finset.cons_induction_on with

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

Goal state before:
pp: α : Type u_1
R : Type u_14
S : Type u_15
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
b : S
s : α →₀ R
f : α → R → S
⊢ b * s.sum f = s.sum fun a c ↦ b * f a c

Tactic:
simp only [Finsupp.sum, Finset.mul_sum]

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
b : β
hb : b ∉ f '' ↑x.support
⊢ (mapDomain f x) b = 0

Tactic:
rw [mapDomain, sum_apply, sum, Finset.sum_eq_zero]
  exact fun a ha ↦ single_eq_of_ne fun eq => hb <| eq ▸ Set.mem_image_of_mem _ ha

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
⊢ sumElim 0 0 = 0

Tactic:
ext (_ | _)

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
val✝ : α
⊢ (sumElim 0 0) (Sum.inl val✝) = 0 (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
val✝ : β
⊢ (sumElim 0 0) (Sum.inr val✝) = 0 (Sum.inr val✝)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
a : α
c : γ
⊢ (single a c).sumElim 0 = single (Sum.inl a) c

Tactic:
ext (_ | _)

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
a : α
c : γ
val✝ : α
⊢ ((single a c).sumElim 0) (Sum.inl val✝) = (single (Sum.inl a) c) (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
a : α
c : γ
val✝ : β
⊢ ((single a c).sumElim 0) (Sum.inr val✝) = (single (Sum.inl a) c) (Sum.inr val✝)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
b : β
c : γ
⊢ sumElim 0 (single b c) = single (Sum.inr b) c

Tactic:
ext (_ | _)

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
b : β
c : γ
val✝ : α
⊢ (sumElim 0 (single b c)) (Sum.inl val✝) = (single (Sum.inr b) c) (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
b : β
c : γ
val✝ : β
⊢ (sumElim 0 (single b c)) (Sum.inr val✝) = (single (Sum.inr b) c) (Sum.inr val✝)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddMonoid M
a : α
b : β
m₁ m₂ : M
⊢ (single a m₁).sumElim (single b m₂) = single (Sum.inl a) m₁ + single (Sum.inr b) m₂

Tactic:
ext (_ | _)

Goal state after:
case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddMonoid M
a : α
b : β
m₁ m₂ : M
val✝ : α
⊢ ((single a m₁).sumElim (single b m₂)) (Sum.inl val✝) = (single (Sum.inl a) m₁ + single (Sum.inr b) m₂) (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddMonoid M
a : α
b : β
m₁ m₂ : M
val✝ : β
⊢ ((single a m₁).sumElim (single b m₂)) (Sum.inr val✝) = (single (Sum.inl a) m₁ + single (Sum.inr b) m₂) (Sum.inr val✝)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α →₀ M
g : β →₀ M
⊢ f.sumElim g = mapDomain Sum.inl f + mapDomain Sum.inr g

Tactic:
ext (_ | _)

Goal state after:
case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α →₀ M
g : β →₀ M
val✝ : α
⊢ (f.sumElim g) (Sum.inl val✝) = (mapDomain Sum.inl f + mapDomain Sum.inr g) (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α →₀ M
g : β →₀ M
val✝ : β
⊢ (f.sumElim g) (Sum.inr val✝) = (mapDomain Sum.inl f + mapDomain Sum.inr g) (Sum.inr val✝)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
a : α →₀ γ
⊢ embDomain Embedding.inl a = a.sumElim 0

Tactic:
ext (_ | _)

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
a : α →₀ γ
val✝ : α
⊢ (embDomain Embedding.inl a) (Sum.inl val✝) = (a.sumElim 0) (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
a : α →₀ γ
val✝ : β
⊢ (embDomain Embedding.inl a) (Sum.inr val✝) = (a.sumElim 0) (Sum.inr val✝)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
b : β →₀ γ
⊢ embDomain Embedding.inr b = sumElim 0 b

Tactic:
ext (_ | _)

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
b : β →₀ γ
val✝ : α
⊢ (embDomain Embedding.inr b) (Sum.inl val✝) = (sumElim 0 b) (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
b : β →₀ γ
val✝ : β
⊢ (embDomain Embedding.inr b) (Sum.inr val✝) = (sumElim 0 b) (Sum.inr val✝)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
c : α ⊕ β →₀ γ
⊢ (comapDomain Sum.inl c ⋯).sumElim (comapDomain Sum.inr c ⋯) = c

Tactic:
ext (_ | _)

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
c : α ⊕ β →₀ γ
val✝ : α
⊢ ((comapDomain Sum.inl c ⋯).sumElim (comapDomain Sum.inr c ⋯)) (Sum.inl val✝) = c (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
c : α ⊕ β →₀ γ
val✝ : β
⊢ ((comapDomain Sum.inl c ⋯).sumElim (comapDomain Sum.inr c ⋯)) (Sum.inr val✝) = c (Sum.inr val✝)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddZeroClass M
a b : α →₀ M
c d : β →₀ M
⊢ (a + b).sumElim (c + d) = a.sumElim c + b.sumElim d

Tactic:
ext (_ | _)

Goal state after:
case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddZeroClass M
a b : α →₀ M
c d : β →₀ M
val✝ : α
⊢ ((a + b).sumElim (c + d)) (Sum.inl val✝) = (a.sumElim c + b.sumElim d) (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddZeroClass M
a b : α →₀ M
c d : β →₀ M
val✝ : β
⊢ ((a + b).sumElim (c + d)) (Sum.inr val✝) = (a.sumElim c + b.sumElim d) (Sum.inr val✝)
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✝³ : CommMonoid M
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
s : Finset ι
b : ι → M
f : ι → N
⊢ ∏ i ∈ s, b i • f i = (∏ i ∈ s, b i) • ∏ i ∈ s, f i

Tactic:
induction s using Finset.cons_induction_on with

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p q : Prop
f : p → M
g : q → M
hpq : p = q
hfg : ∀ (h : q), f ⋯ = g h
⊢ finprod f = finprod g

Tactic:
by
  subst q
  exact finprod_congr hfg

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ val '' Ici i = Ico (↑i) n

Tactic:
← preimage_val_Ici_val,

Goal state after:
n : ℕ
i : Fin n
⊢ val '' val ⁻¹' Ici ↑i = Ico (↑i) n
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
x : α
hx : x ∈ s ∩ mulSupport f
⊢ x ∈ ↑t

Tactic:
exact (h hx.2).1 hx.1

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

Goal state before:
pp: ι : 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✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
⊢ b.reindexFinsetRange.repr (b i) = single ⟨b i, ⋯⟩ 1

Tactic:
by
  ext ⟨bi, hbi⟩
  rw [reindexFinsetRange, repr_reindex, Finsupp.mapDomain_equiv_apply, reindexRange_repr_self]
  simp [Finsupp.single_apply]

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:
by
            rw [LinearMap.comp_apply, b.constr_basis, Function.comp_apply, ← hi', b'.constr_basis,
              Function.comp_apply, hi', hgf, LinearMap.id_apply]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
⊢ (∃ n f g, ∑ i, f i • ↑(g i) = m) ↔ ∃ i x, (∀ (i : Fin i), (x i).2 ∈ s) ∧ ∑ i, (x i).1 • (x i).2 = m

Tactic:
refine exists_congr (fun n ↦ ⟨?_, ?_⟩)

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
n : ℕ
⊢ (∃ f g, ∑ i, f i • ↑(g i) = m) → ∃ x, (∀ (i : Fin n), (x i).2 ∈ s) ∧ ∑ i, (x i).1 • (x i).2 = m

case refine_2
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
n : ℕ
⊢ (∃ x, (∀ (i : Fin n), (x i).2 ∈ s) ∧ ∑ i, (x i).1 • (x i).2 = m) → ∃ f g, ∑ i, f i • ↑(g i) = m
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x : ℕ∞
⊢ x ^ 0 = 1

Tactic:
← natCast_zero,

Goal state after:
x : ℕ∞
⊢ x ^ ↑0 = 1
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ LinearIndependent R v ↔
    ∀ (s : Finset ι) (f g : ι → R),
      (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i

Tactic:
exact linearIndependent_iff'ₛ.trans
    ⟨fun H s f g eq hv i ↦ if his : i ∈ s then H s f g hv i his else eq i his,
      fun H s f g eq i hi ↦ by
      convert!
        H s (fun j ↦ if j ∈ s then f j else 0) (fun j ↦ if j ∈ s then g j else 0)
          (fun j hj ↦ (if_neg hj).trans (if_neg hj).symm)
          (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]) i <;>
      exact (if_pos hi).symm⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a : G
⊢ a ≡ 0 [PMOD p] ↔ ∃ z, a = z • p

Tactic:
rw [modEq_comm, modEq_iff_eq_add_zsmul]

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
p a : G
⊢ (∃ z, a = 0 + z • p) ↔ ∃ z, a = z • p
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr.inr.inr.inl
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : c < b
⊢ a ^ c - 1 < a ^ b - 1

Tactic:
rwa [Nat.sub_lt_sub_iff_right (one_le_pow c a ha0), Nat.pow_lt_pow_iff_right ha1]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr.inr.inr.inl
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : c < b
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

pp: case inr.inr.inr.inr
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
· rw [mod_eq_of_lt, mod_eq_of_lt h]
    rwa [Nat.sub_lt_sub_iff_right (one_le_pow c a ha0), Nat.pow_lt_pow_iff_right ha1]

Goal state after:
case inr.inr.inr.inr
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b n : ℕ
hn : 0 < n.succ
⊢ (a ^ n * a).Coprime b ↔ a.Coprime b

Tactic:
Nat.coprime_mul_iff_left

Goal state after:
a b n : ℕ
hn : 0 < n.succ
⊢ (a ^ n).Coprime b ∧ a.Coprime b ↔ a.Coprime b
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b : ℕ
⊢ a ≡ b [MOD n] ↔ ↑n ∣ ↑b - ↑a

Tactic:
by
  rw [ModEq, eq_comm, ← Int.natCast_inj, Int.natCast_mod, Int.natCast_mod,
    Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.dvd_iff_emod_eq_zero]

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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
h_total_l : (Finsupp.linearCombination R v) l = v i
h_total_eq : (Finsupp.linearCombination R v) l = (Finsupp.linearCombination R v) (Finsupp.single i 1)
l_eq : Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩) = Finsupp.single i 1
⊢ ∃ a, f a = i

Tactic:
← Finsupp.embDomain_eq_mapDomain

Goal state after:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
h_total_l : (Finsupp.linearCombination R v) l = v i
h_total_eq : (Finsupp.linearCombination R v) l = (Finsupp.linearCombination R v) (Finsupp.single i 1)
l_eq : Finsupp.embDomain f (repr ⟨v i, ⋯⟩) = Finsupp.single i 1
⊢ ∃ a, f a = i
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ n)
b : Fin n
⊢ ↑a / m ^ ↑b % m < m

Tactic:
rcases n with - | n
      · exact b.elim0
      rcases m with - | m
      · rw [zero_pow n.succ_ne_zero] at a
        exact a.elim0
      · exact Nat.mod_lt _ m.succ_pos

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

Goal state before:
pp: case neg
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : ¬c ≤ a % c + b % c
⊢ (a % c + b % c) % c + 0 = a % c + b % c

Tactic:
rw [Nat.mod_eq_of_lt (lt_of_not_ge h), add_zero]

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

Goal state before:
pp: case refine_2.inr
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : ∀ x ∈ span R (v '' range Sum.inl), ∀ y ∈ span R (v '' range Sum.inr), x = y → x = 0
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
this :
  ∑ i ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl i) =
    -∑ i ∈ s.preimage Sum.inr ⋯, (fun x ↦ g x • v x) (Sum.inr i)
A : ∑ c ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl c) = 0
i : ι'
hi : Sum.inr i ∈ s
⊢ g (Sum.inr i) = 0

Tactic:
rw [this, neg_eq_zero] at A
    exact hr _ _ A i (Finset.mem_preimage.2 hi)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
⊢ Bijective f ↔ Injective f ∧ Nat.card α = Nat.card β

Tactic:
Bijective,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
⊢ Bijective f ↔ Nat.card α = Nat.card β ∧ Surjective f

Tactic:
Bijective,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
⊢ Injective f ∧ Surjective f ↔ Nat.card α = Nat.card β ∧ Surjective f