harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.comap (f : β → α) (hl : l.HasBasis p s) :
    (l.comap f).HasBasis p fun i => f ⁻¹' s i :=
  ⟨fun t => by
    simp only [mem_comap', hl.mem_iff]
    refine exists_congr (fun i => Iff.rfl.and ?_)
    exact ⟨fun h x hx => h hx rfl, fun h y hy x hx => h <| by rwa [mem_preimage, hx]⟩⟩

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
i : ι
⊢ s i ⊆ {y | ∀ ⦃x : β⦄, f x = y → x ∈ t} ↔ f ⁻¹' s i ⊆ t

Tactic:
exact ⟨fun h x hx => h hx rfl, fun h y hy x hx => h <| by rwa [mem_preimage, hx]⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
⊢ t ∈ Filter.comap f l ↔ ∃ i, p i ∧ f ⁻¹' s i ⊆ t

Tactic:
simp only [mem_comap', hl.mem_iff]

Result:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
⊢ (∃ i, p i ∧ s i ⊆ {y | ∀ ⦃x : β⦄, f x = y → x ∈ t}) ↔ ∃ i, p i ∧ f ⁻¹' s i ⊆ t

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
⊢ (∃ i, p i ∧ s i ⊆ {y | ∀ ⦃x : β⦄, f x = y → x ∈ t}) ↔ ∃ i, p i ∧ f ⁻¹' s i ⊆ t

Tactic:
refine exists_congr (fun i => Iff.rfl.and ?_)

Result:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
i : ι
⊢ s i ⊆ {y | ∀ ⦃x : β⦄, f x = y → x ∈ t} ↔ f ⁻¹' s i ⊆ t

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
i : ι
h : f ⁻¹' s i ⊆ t
y : α
hy : y ∈ s i
x : β
hx : f x = y
⊢ x ∈ f ⁻¹' s i

Tactic:
rwa [mem_preimage, hx]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Mono.lean
theorem epi_of_isColimitMkIdId (f : X ⟶ Y)
    (t : IsColimit (mk (𝟙 Y) (𝟙 Y) rfl : PushoutCocone f f)) : Epi f :=
  ⟨fun {Z} g h eq => by
    rcases PushoutCocone.IsColimit.desc' t _ _ eq with ⟨_, rfl, rfl⟩
    rfl⟩

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsColimit (mk (𝟙 Y) (𝟙 Y) ⋯)
Z : C
g h : Y ⟶ Z
eq : f ≫ g = f ≫ h
⊢ g = h

Tactic:
rcases PushoutCocone.IsColimit.desc' t _ _ eq with ⟨_, rfl, rfl⟩

Result:
case mk.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsColimit (mk (𝟙 Y) (𝟙 Y) ⋯)
Z : C
val✝ : (mk (𝟙 Y) (𝟙 Y) ⋯).pt ⟶ Z
eq : f ≫ (mk (𝟙 Y) (𝟙 Y) ⋯).inl ≫ val✝ = f ≫ (mk (𝟙 Y) (𝟙 Y) ⋯).inr ≫ val✝
⊢ (mk (𝟙 Y) (𝟙 Y) ⋯).inl ≫ val✝ = (mk (𝟙 Y) (𝟙 Y) ⋯).inr ≫ val✝

Proof state:
case mk.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsColimit (mk (𝟙 Y) (𝟙 Y) ⋯)
Z : C
val✝ : (mk (𝟙 Y) (𝟙 Y) ⋯).pt ⟶ Z
eq : f ≫ (mk (𝟙 Y) (𝟙 Y) ⋯).inl ≫ val✝ = f ≫ (mk (𝟙 Y) (𝟙 Y) ⋯).inr ≫ val✝
⊢ (mk (𝟙 Y) (𝟙 Y) ⋯).inl ≫ val✝ = (mk (𝟙 Y) (𝟙 Y) ⋯).inr ≫ val✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/Floor/Div.lean
@[simp] lemma floorDiv_one [Nontrivial α] (b : β) : b ⌊/⌋ (1 : α) = b :=
  eq_of_forall_le_iff <| fun c ↦ by simp [zero_lt_one' α]

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : OrderedSemiring α
inst✝³ : OrderedAddCommMonoid β
inst✝² : MulActionWithZero α β
inst✝¹ : FloorDiv α β
inst✝ : Nontrivial α
b c : β
⊢ c ≤ b ⌊/⌋ 1 ↔ c ≤ b

Tactic:
simp [zero_lt_one' α]

Result:
no goals
-- Mathlib/Algebra/Order/Quantale.lean
theorem leftMulResiduation_le_iff_mul_le : x ≤ y ⇨ₗ z ↔ x * y ≤ z where
  mp h1

Proof state:
α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
h1 : x ≤ y ⇨ₗ z
⊢ (y ⇨ₗ z) * y ≤ z

Tactic:
simp_all only [leftMulResiduation, sSup_mul_distrib, Set.mem_setOf_eq,
  iSup_le_iff, implies_true]

Result:
no goals

Proof state:
α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
h1 : x ≤ y ⇨ₗ z
⊢ x * y ≤ z

Tactic:
apply le_trans (mul_le_mul_right' h1 _)

Result:
α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
h1 : x ≤ y ⇨ₗ z
⊢ (y ⇨ₗ z) * y ≤ z
-- Mathlib/Order/CompleteLattice.lean
theorem Antitone.map_sSup_le [CompleteLattice β] {s : Set α} {f : α → β} (hf : Antitone f) :
    f (sSup s) ≤ ⨅ a ∈ s, f a

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
s : Set α
f : α → β
hf : Antitone f
⊢ f (⨆ a ∈ s, a) ≤ ⨅ a ∈ s, f a

Tactic:
exact hf.map_iSup₂_le _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
s : Set α
f : α → β
hf : Antitone f
⊢ f (sSup s) ≤ ⨅ a ∈ s, f a

Tactic:
rw [sSup_eq_iSup]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
s : Set α
f : α → β
hf : Antitone f
⊢ f (⨆ a ∈ s, a) ≤ ⨅ a ∈ s, f a
-- Mathlib/Algebra/Polynomial/Eval/Algebra.lean
theorem eval₂_pow' (n : ℕ) :
    (p ^ n).eval₂ (algebraMap R S) x = (p.eval₂ (algebraMap R S) x) ^ n

Proof state:
case zero
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p : R[X]
⊢ eval₂ (algebraMap R S) x (p ^ 0) = eval₂ (algebraMap R S) x p ^ 0

Tactic:
simp only [pow_zero, eval₂_one]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p : R[X]
n : ℕ
⊢ eval₂ (algebraMap R S) x (p ^ n) = eval₂ (algebraMap R S) x p ^ n

Tactic:
induction n with
| zero => simp only [pow_zero, eval₂_one]
| succ n ih => rw [pow_succ, pow_succ, eval₂_mul', ih]

Result:
no goals

Proof state:
case succ
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p : R[X]
n : ℕ
ih : eval₂ (algebraMap R S) x (p ^ n) = eval₂ (algebraMap R S) x p ^ n
⊢ eval₂ (algebraMap R S) x (p ^ (n + 1)) = eval₂ (algebraMap R S) x p ^ (n + 1)

Tactic:
rw [pow_succ, pow_succ, eval₂_mul', ih]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem singleton_inj : #[a] = #[b] ↔ a = b

Proof state:
α✝ : Type u_1
a b : α✝
⊢ #[a] = #[b] ↔ a = b

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem strictMono_mersenne : StrictMono mersenne := fun m n h ↦
  (Nat.sub_lt_sub_iff_right <| Nat.one_le_pow _ _ two_pos).2 <| by gcongr; norm_num1

Proof state:
case h
m n : ℕ
h : m < n
⊢ 1 < 2

Tactic:
norm_num1

Result:
no goals

Proof state:
m n : ℕ
h : m < n
⊢ 2 ^ m < 2 ^ n

Tactic:
gcongr

Result:
case h
m n : ℕ
h : m < n
⊢ 1 < 2
-- Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
theorem card_div_mul_le_card_div_mul_card_mul (A B C : Finset G) :
    #(A / C) * #B ≤ #(A / B) * #(B * C)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A * C⁻¹) * #B ≤ #(A / B) * #(B / C⁻¹)

Tactic:
exact ruzsa_triangle_inequality_mul_div_div _ _ _

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A / C) * #B ≤ #(A / B) * #(B * C)

Tactic:
rw [← div_inv_eq_mul, div_eq_mul_inv]

Result:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A * C⁻¹) * #B ≤ #(A / B) * #(B / C⁻¹)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem pmap_mk {xs : Array α} {h : xs.size = n} {P : α → Prop} {f : ∀ a, P a → β}
    {H : ∀ a ∈ mk xs h, P a} :
    (mk xs h).pmap f H = mk (xs.pmap f (by simpa using H)) (by simpa using h)

Proof state:
α : Type ?u.2431
n : Nat
β : Type ?u.2505
xs : Array α
h : xs.size = n
P : α → Prop
f : (a : α) → P a → β
H : ∀ (a : α), a ∈ { toArray := xs, size_toArray := h } → P a
⊢ (Array.pmap f xs ⋯).size = n

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type ?u.2431
n : Nat
β : Type ?u.2505
xs : Array α
h : xs.size = n
P : α → Prop
f : (a : α) → P a → β
H : ∀ (a : α), a ∈ { toArray := xs, size_toArray := h } → P a
⊢ ∀ (a : α), a ∈ xs → P a

Tactic:
simpa using H

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
xs : Array α
h : xs.size = n
P : α → Prop
f : (a : α) → P a → β
H : ∀ (a : α), a ∈ { toArray := xs, size_toArray := h } → P a
⊢ pmap f { toArray := xs, size_toArray := h } H = { toArray := Array.pmap f xs ⋯, size_toArray := ⋯ }

Tactic:
simp [pmap]

Result:
no goals
-- Mathlib/Tactic/Module.lean
theorem smul_eq_eval {R₀ : Type*} [AddCommMonoid M] [Semiring R] [Module R M] [Semiring R₀]
    [Module R₀ M] [Semiring S] [Module S M]  {l : NF R M} {l₀ : NF R₀ M} {s : S} {r : R}
    {x : M} (hx : x = l₀.eval) (hl : l.eval = l₀.eval) (hs : r • x = s • x) :
    s • x = (r • l).eval

Proof state:
S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₀
inst✝² : Module R₀ M
inst✝¹ : Semiring S
inst✝ : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ s • x = (r • l).eval

Tactic:
rw [← hs, hx, ← hl, eval_smul]

Result:
case h
S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₀
inst✝² : Module R₀ M
inst✝¹ : Semiring S
inst✝ : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ l.eval = l.eval

Proof state:
case h
S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₀
inst✝² : Module R₀ M
inst✝¹ : Semiring S
inst✝ : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ l.eval = l.eval

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem gcd_dvd_left : gcd x y ∣ x :=
  (Submodule.IsPrincipal.mem_iff_generator_dvd _).mp (Ideal.subset_span (by simp))

Proof state:
R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ x ∈ {x, y}

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem map.comp {γ : Type w} (f : α → β) (g : β → γ) (x) :
    map g (map f x) = map (g ∘ f) x

Proof state:
case mk
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeGroup α
L : List (α × Bool)
⊢ (map g) ((map f) (Quot.mk Red.Step L)) = (map (g ∘ f)) (Quot.mk Red.Step L)

Tactic:
simp [Function.comp_def]

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeGroup α
⊢ (map g) ((map f) x) = (map (g ∘ f)) x

Tactic:
rcases x with ⟨L⟩

Result:
case mk
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeGroup α
L : List (α × Bool)
⊢ (map g) ((map f) (Quot.mk Red.Step L)) = (map (g ∘ f)) (Quot.mk Red.Step L)
-- Mathlib/RingTheory/Ideal/Over.lean
theorem LiesOver.of_eq_map_equiv [P.LiesOver p] {E : Type*} [EquivLike E B C]
    [AlgEquivClass E A B C] (σ : E) (h : Q = P.map σ) : Q.LiesOver p

Proof state:
A : Type u_2
inst✝⁷ : CommSemiring A
B : Type u_3
C : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra A B
inst✝³ : Algebra A C
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝² : P.LiesOver p
E : Type u_5
inst✝¹ : EquivLike E B C
inst✝ : AlgEquivClass E A B C
σ : E
h : Q = comap (↑σ).symm P
⊢ Q.LiesOver p

Tactic:
exact of_eq_comap p (σ : B ≃ₐ[A] C).symm h

Result:
no goals

Proof state:
A : Type u_2
inst✝⁷ : CommSemiring A
B : Type u_3
C : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra A B
inst✝³ : Algebra A C
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝² : P.LiesOver p
E : Type u_5
inst✝¹ : EquivLike E B C
inst✝ : AlgEquivClass E A B C
σ : E
h : Q = map σ P
⊢ Q.LiesOver p

Tactic:
rw [← show _ = P.map σ from comap_symm (σ : B ≃+* C)] at h

Result:
A : Type u_2
inst✝⁷ : CommSemiring A
B : Type u_3
C : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra A B
inst✝³ : Algebra A C
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝² : P.LiesOver p
E : Type u_5
inst✝¹ : EquivLike E B C
inst✝ : AlgEquivClass E A B C
σ : E
h : Q = comap (↑σ).symm P
⊢ Q.LiesOver p
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem brange_bfamilyOfFamily' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) :
    brange _ (bfamilyOfFamily' r f) = range f

Proof state:
case refine_1.intro.intro
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
i : Ordinal.{u}
hi : i < type r
⊢ bfamilyOfFamily' r f i hi ∈ range f

Tactic:
apply mem_range_self

Result:
no goals

Proof state:
case refine_1
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
a : α
⊢ a ∈ (type r).brange (bfamilyOfFamily' r f) → a ∈ range f

Tactic:
rintro ⟨i, hi, rfl⟩

Result:
case refine_1.intro.intro
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
i : Ordinal.{u}
hi : i < type r
⊢ bfamilyOfFamily' r f i hi ∈ range f

Proof state:
case refine_2.intro
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
b : ι
⊢ f b ∈ (type r).brange (bfamilyOfFamily' r f)

Tactic:
exact ⟨_, _, bfamilyOfFamily'_typein _ _ _⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
a : α
⊢ a ∈ range f → a ∈ (type r).brange (bfamilyOfFamily' r f)

Tactic:
rintro ⟨b, rfl⟩

Result:
case refine_2.intro
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
b : ι
⊢ f b ∈ (type r).brange (bfamilyOfFamily' r f)

Proof state:
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
⊢ (type r).brange (bfamilyOfFamily' r f) = range f

Tactic:
refine Set.ext fun a => ⟨?_, ?_⟩

Result:
case refine_1
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
a : α
⊢ a ∈ (type r).brange (bfamilyOfFamily' r f) → a ∈ range f

case refine_2
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
a : α
⊢ a ∈ range f → a ∈ (type r).brange (bfamilyOfFamily' r f)
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem sup_h_of_disjoint (f g : E →ₗ.[R] F) (h : Disjoint f.domain g.domain) (x : f.domain)
    (y : g.domain) (hxy : (x : E) = y) : f x = g y

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ x ∈ f.domain, x ∈ g.domain → x = 0
x : ↥f.domain
y : ↥g.domain
hxy : ↑x = ↑y
⊢ ↑f x = ↑g y

Tactic:
have hy : y = 0 := Subtype.eq (h y (hxy ▸ x.2) y.2)

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ x ∈ f.domain, x ∈ g.domain → x = 0
x : ↥f.domain
y : ↥g.domain
hxy : ↑x = ↑y
hy : y = 0
⊢ ↑f x = ↑g y

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ x ∈ f.domain, x ∈ g.domain → x = 0
x : ↥f.domain
y : ↥g.domain
hxy : ↑x = ↑y
hy : y = 0
⊢ ↑f x = ↑g y

Tactic:
have hx : x = 0 := Subtype.eq (hxy.trans <| congr_arg _ hy)

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ x ∈ f.domain, x ∈ g.domain → x = 0
x : ↥f.domain
y : ↥g.domain
hxy : ↑x = ↑y
hy : y = 0
hx : x = 0
⊢ ↑f x = ↑g y

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : Disjoint f.domain g.domain
x : ↥f.domain
y : ↥g.domain
hxy : ↑x = ↑y
⊢ ↑f x = ↑g y

Tactic:
rw [disjoint_def] at h

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ x ∈ f.domain, x ∈ g.domain → x = 0
x : ↥f.domain
y : ↥g.domain
hxy : ↑x = ↑y
⊢ ↑f x = ↑g y

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ x ∈ f.domain, x ∈ g.domain → x = 0
x : ↥f.domain
y : ↥g.domain
hxy : ↑x = ↑y
hy : y = 0
hx : x = 0
⊢ ↑f x = ↑g y

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
/-- A partial homeomorphism is an open map on its source:
  the image of an open subset of the source is open. -/
lemma isOpen_image_of_subset_source {s : Set X} (hs : IsOpen s) (hse : s ⊆ e.source) :
    IsOpen (e '' s)

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Set X
hs : IsOpen s
hse : s ⊆ e.source
⊢ IsOpen (e.target ∩ ↑e.symm ⁻¹' s)

Tactic:
exact e.continuousOn_invFun.isOpen_inter_preimage e.open_target hs

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Set X
hs : IsOpen s
hse : s ⊆ e.source
⊢ IsOpen (↑e '' s)

Tactic:
rw [(image_eq_target_inter_inv_preimage (e := e) hse)]

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Set X
hs : IsOpen s
hse : s ⊆ e.source
⊢ IsOpen (e.target ∩ ↑e.symm ⁻¹' s)
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem map_of_injective [MonoidHomClass F M N] (h : IsPrimitiveRoot ζ k) (hf : Injective f) :
    IsPrimitiveRoot (f ζ) k where
  pow_eq_one

Proof state:
M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
⊢ ∀ (l : ℕ), f ζ ^ l = 1 → orderOf ζ ∣ l

Tactic:
intro l hl

Result:
M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
l : ℕ
hl : f ζ ^ l = 1
⊢ orderOf ζ ∣ l

Proof state:
M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
⊢ f ζ ^ k = 1

Tactic:
rw [← map_pow, h.pow_eq_one, map_one]

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
l : ℕ
hl : f (ζ ^ l) = f 1
⊢ orderOf ζ ∣ l

Tactic:
exact orderOf_dvd_of_pow_eq_one (hf hl)

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
l : ℕ
hl : f ζ ^ l = 1
⊢ orderOf ζ ∣ l

Tactic:
rw [← map_pow, ← map_one f] at hl

Result:
M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
l : ℕ
hl : f (ζ ^ l) = f 1
⊢ orderOf ζ ∣ l

Proof state:
M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
⊢ ∀ (l : ℕ), f ζ ^ l = 1 → k ∣ l

Tactic:
rw [h.eq_orderOf]

Result:
M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
⊢ ∀ (l : ℕ), f ζ ^ l = 1 → orderOf ζ ∣ l
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem foldl_attach (l : Array α) (f : β → α → β) (b : β) :
    l.attach.foldl (fun acc t => f acc t.1) b = l.foldl f b

Proof state:
case mk.e_a
α : Type u_1
β : Type u_2
f : β → α → β
b : β
l : List α
⊢ (List.pmap (fun a h => ⟨a, ⋯⟩) l ⋯).unattach = l

Tactic:
ext

Result:
case mk.e_a.h.a
α : Type u_1
β : Type u_2
f : β → α → β
b : β
l : List α
i✝ : Nat
a✝ : α
⊢ a✝ ∈ (List.pmap (fun a h => ⟨a, ⋯⟩) l ⋯).unattach[i✝]? ↔ a✝ ∈ l[i✝]?

Proof state:
case mk
α : Type u_1
β : Type u_2
f : β → α → β
b : β
l : List α
⊢ List.foldl f b (List.pmap (fun a h => ⟨a, ⋯⟩) l ⋯).unattach = List.foldl f b l

Tactic:
congr

Result:
case mk.e_a
α : Type u_1
β : Type u_2
f : β → α → β
b : β
l : List α
⊢ (List.pmap (fun a h => ⟨a, ⋯⟩) l ⋯).unattach = l

Proof state:
case mk
α : Type u_1
β : Type u_2
f : β → α → β
b : β
l : List α
⊢ foldl (fun acc t => f acc t.val) b { toList := l }.attach = foldl f b { toList := l }

Tactic:
simp only [List.attach_toArray, List.attachWith_mem_toArray, List.map_attach, size_toArray,
  List.length_pmap, List.foldl_toArray', mem_toArray, List.foldl_subtype]

Result:
case mk
α : Type u_1
β : Type u_2
f : β → α → β
b : β
l : List α
⊢ List.foldl f b (List.pmap (fun a h => ⟨a, ⋯⟩) l ⋯).unattach = List.foldl f b l

Proof state:
case mk.e_a.h.a
α : Type u_1
β : Type u_2
f : β → α → β
b : β
l : List α
i✝ : Nat
a✝ : α
⊢ a✝ ∈ (List.pmap (fun a h => ⟨a, ⋯⟩) l ⋯).unattach[i✝]? ↔ a✝ ∈ l[i✝]?

Tactic:
simpa using fun a => List.mem_of_getElem? a

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : β → α → β
b : β
⊢ foldl (fun acc t => f acc t.val) b l.attach = foldl f b l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : β → α → β
b : β
l : List α
⊢ foldl (fun acc t => f acc t.val) b { toList := l }.attach = foldl f b { toList := l }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.of_lo_eq_false_1 (u v : Nat) : ((u + 1 ≤ v) = False) → v ≤ u

Proof state:
u v : Nat
⊢ (u + 1 ≤ v) = False → v ≤ u

Tactic:
simp

Result:
u v : Nat
⊢ v < u + 1 → v ≤ u

Proof state:
u v : Nat
⊢ v < u + 1 → v ≤ u

Tactic:
omega

Result:
no goals
-- Mathlib/Data/List/GetD.lean
theorem getD_eq_default {n : ℕ} (hn : l.length ≤ n) : l.getD n d = d

Proof state:
case cons.zero
α : Type u
l : List α
d head : α
tail : List α
ih : ∀ {n : ℕ}, tail.length ≤ n → tail.getD n d = d
hn : (head :: tail).length ≤ 0
⊢ (head :: tail).getD 0 d = d

Tactic:
simp at hn

Result:
no goals

Proof state:
case cons
α : Type u
l : List α
d head : α
tail : List α
ih : ∀ {n : ℕ}, tail.length ≤ n → tail.getD n d = d
n : ℕ
hn : (head :: tail).length ≤ n
⊢ (head :: tail).getD n d = d

Tactic:
cases n

Result:
case cons.zero
α : Type u
l : List α
d head : α
tail : List α
ih : ∀ {n : ℕ}, tail.length ≤ n → tail.getD n d = d
hn : (head :: tail).length ≤ 0
⊢ (head :: tail).getD 0 d = d

case cons.succ
α : Type u
l : List α
d head : α
tail : List α
ih : ∀ {n : ℕ}, tail.length ≤ n → tail.getD n d = d
n✝ : ℕ
hn : (head :: tail).length ≤ n✝ + 1
⊢ (head :: tail).getD (n✝ + 1) d = d

Proof state:
case cons.succ
α : Type u
l : List α
d head : α
tail : List α
ih : ∀ {n : ℕ}, tail.length ≤ n → tail.getD n d = d
n✝ : ℕ
hn : (head :: tail).length ≤ n✝ + 1
⊢ (head :: tail).getD (n✝ + 1) d = d

Tactic:
exact ih (Nat.le_of_succ_le_succ hn)

Result:
no goals

Proof state:
case nil
α : Type u
l : List α
d : α
n : ℕ
hn : [].length ≤ n
⊢ [].getD n d = d

Tactic:
exact getD_nil

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_pos_iff (hx : 0 < x) : 0 < logb b x ↔ 1 < x

Proof state:
b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b 1 < logb b x ↔ 1 < x

Tactic:
rw [logb_lt_logb_iff hb zero_lt_one hx]

Result:
no goals

Proof state:
b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ 0 < logb b x ↔ 1 < x

Tactic:
rw [← @logb_one b]

Result:
b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b 1 < logb b x ↔ 1 < x
-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem cRk_restrict (M : Matroid α) (X Y : Set α) : (M ↾ X).cRk Y = M.cRk (X ∩ Y)

Proof state:
α : Type u
M : Matroid α
X Y : Set α
⊢ (M ↾ X).cRk Y = M.cRk (X ∩ Y)

Tactic:
rw [← cRk_inter_ground, restrict_ground_eq, cRk_restrict_subset _ inter_subset_right,
  inter_comm]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem sum_blocksFun : ∑ i, c.blocksFun i = n

Proof state:
n : ℕ
c : Composition n
⊢ ∑ i : Fin c.length, c.blocksFun i = n

Tactic:
conv_rhs => rw [← c.blocks_sum, ← ofFn_blocksFun, sum_ofFn]

Result:
no goals